Abstract Well-founded recursion generalises both strong induction and recursion. In this post we’ll: Discuss the (informal) notion of a well-founded relation. Show how to use well-founded relations (initially just with the < relation on ℕ) to define recursive functions and prove theorems using the equation compiler and by writing proof terms. Explain why rfl proofs […]

## Well-founded recursion

- Post author By Gihan Marasingha
- Post date
- Categories In Fundamental concepts
- No Comments on Well-founded recursion