Reasoning with inductive types

Introduction Inductive types are very powerful because they allow to write recursively defined functions which are guaranteed to terminate and to reason about them by induction. Recursively defined functions an proofs by induction are closely related. As an introductory example we use the class case class UNARY_NATURAL create zero succ(pred: UNARY_NATURAL) feature plus alias “+” […]