search

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.
https://leanprover-community.github.io/
MIT License
51 stars 119 forks source link

Update "Well-founded Recursion" for Lean 4 #483

Closed Komyyy closed 1 month ago

semorrison commented 1 month ago

@nomeata, could you comment here on what is available in the official documentation / blog posts? We would prefer to simply not have the content on the community webpage at all.

If there is existing material we can simply link to, we will do that.

If you were able to look at this PR and make sure that all content is reflected somewhere more official, that would be ideal.

nomeata commented 1 month ago

We have the blog post https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/, not sure what else we do. I expect this will improve with the reference manual.