Hi, I have been working on a tutorial about Equations and well-founded recursion.
It is not done yet, but if you wish, you can already check it out and give back informal feedback here.
To finish it, I am lacking some examples. Would anyone have an idea ?
f : nat -> A
so size is not an integer or sth like that ?map_in
trick like discussed here The tuto on wf is ready to be reviewed.
It has been split in two with a tutorial dedicated to obligations and Equations.
Last updated: Oct 13 2024 at 01:02 UTC