Tag: Equation compiler

Well-founded recursion

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 […]