From e93a924d196e2ed001fb60386758884bc9d1f0f5 Mon Sep 17 00:00:00 2001 From: Stan Manilov Date: Tue, 27 May 2025 17:43:51 +0300 Subject: [PATCH] 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. --- src/solve/coinduction.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solve/coinduction.md b/src/solve/coinduction.md index c682e002d..9753f7539 100644 --- a/src/solve/coinduction.md +++ b/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: 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: [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