We implement natural numbers, arithmetic and comparison using an inductive datatype. All code can be found in the course git repository github.com/MariusFurter/MAT60...
00:00 Introduction
00:14 data Nat
03:10 Conversion functions
10:14 Arithmetic functions
21:21 Comparison functions
30:46 Folding over Nat
The playlist for the course can be found here: • Logic & Foundations wi...