coq / platform-docs

A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
https://coq.inria.fr/platform-docs/
Other
19 stars 11 forks source link

Tutorial, Equations: well-founded recursion #2

Closed thomas-lamiaux closed 5 months ago

thomas-lamiaux commented 6 months ago

A tutorial explaining how to use Equations to define functions by well-founded recursion, and how to reason about such functions.

There is left to :

thomas-lamiaux commented 6 months ago

There is currently an issue with Ack to solve. We are waiting for this fix to funelim to be integrated to investigate it.

thomas-lamiaux commented 5 months ago

I have made mistakes with git. As I don't know how to solve them, I have reopened a cleaner new PR.