flâneur

On Well-Founded Induction

boarders.github.io · 7,420 words · saved by 1 readers

Callan McGillx

One of the first things dependently typed programming teaches is that thinking of induction as primarily about the natural numbers is an impoverished view. Instead, a proof assistant like agda encourages one firstly towards the idea that mathematics can be founded on inductive structures as the raw primitives, and secondly that every such structure comes with some given means of proving properties about it. For instance, binary trees in agda might be defined as follows: data BinTree ( a : Type ) : Type where Leaf : a → BinTree a Bin : BinTree a → BinTree a → BinTree a and these come with the f

saved by

related reading