diff options
| author | nora <48135649+Noratrieb@users.noreply.github.com> | 2025-05-27 18:53:29 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-05-27 18:53:29 +0200 |
| commit | a07a972e2df7f99874d73ebec922d303aa24de0b (patch) | |
| tree | 25198dc92737a9528e018464d4bdda2431a34391 /src/doc | |
| parent | 58e5e32fbee5d7e5eb0fff30bb954f22395221f3 (diff) | |
| parent | a5c16e6cb82d5e5d53e43f9d5f7aeb68c676ddda (diff) | |
| download | rust-a07a972e2df7f99874d73ebec922d303aa24de0b.tar.gz rust-a07a972e2df7f99874d73ebec922d303aa24de0b.zip | |
Merge pull request #2417 from smanilov/patch-16
Make links in coinduction.md clickable
Diffstat (limited to 'src/doc')
| -rw-r--r-- | src/doc/rustc-dev-guide/src/solve/coinduction.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/doc/rustc-dev-guide/src/solve/coinduction.md b/src/doc/rustc-dev-guide/src/solve/coinduction.md index c682e002db7..9753f7539c2 100644 --- a/src/doc/rustc-dev-guide/src/solve/coinduction.md +++ b/src/doc/rustc-dev-guide/src/solve/coinduction.md @@ -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 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. - 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 - 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 [ex1]: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0a9c3830b93a2380e6978d6328df8f72 |