mirror
/
rustc-dev-guide
mirror of https://github.com/rust-lang/rustc-dev-guide.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Make links in coinduction.md clickable 

Although they are clickable in the github preview, they aren't in the actual rendered HTML on https://rustc-dev-guide.rust-lang.org/.

This commit fixes that.
This commit is contained in:
Stan Manilov 2025-05-27 17:43:51 +03:00
parent a20005c9ec
commit e93a924d19
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/solve/coinduction.md
View File

@ -237,14 +237,14 @@ Alternatively, we could simply always treat the equate branch of `normalizes_to`
Any cycles should result in infinite types, which aren't supported anyways and would only Any cycles should result in infinite types, which aren't supported anyways and would only
result in overflow when deeply normalizing for codegen. result in overflow when deeply normalizing for codegen.
experimentation and examples: https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view experimentation and examples: <https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view>
Another attempt at a summary. Another attempt at a summary.
- in projection eq, we must make progress with constraining the rhs - in projection eq, we must make progress with constraining the rhs
- a cycle is only ok if while equating we have a rigid ty on the lhs after norm at least once - a cycle is only ok if while equating we have a rigid ty on the lhs after norm at least once
- cycles outside of the recursive `eq` call of `normalizes_to` are always fine - cycles outside of the recursive `eq` call of `normalizes_to` are always fine
[^1]: related: https://coq.inria.fr/refman/language/core/coinductive.html#top-level-definitions-of-corecursive-functions [^1]: related: <https://coq.inria.fr/refman/language/core/coinductive.html#top-level-definitions-of-corecursive-functions>
[perfect derive]: https://smallcultfollowing.com/babysteps/blog/2022/04/12/implied-bounds-and-perfect-derive [perfect derive]: https://smallcultfollowing.com/babysteps/blog/2022/04/12/implied-bounds-and-perfect-derive
[ex1]: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0a9c3830b93a2380e6978d6328df8f72 [ex1]: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0a9c3830b93a2380e6978d6328df8f72