It's the traditional, inductive definition of natural numbers. You give a base c...

		gnuvince on April 13, 2014 \| parent \| context \| favorite \| on: Try Idris It's the traditional, inductive definition of natural numbers. You give a base case (Z = Zero) and an inductive case (S Nat = Successor of Nat). So Z is a natural number, S Z is also a natural number and corresponds to 1, S (S Z) corresponds to 2, etc.