Feb 16, 2022
(* Type definition for Church numerals. *)
Definition cnat := forall X : Type, (X -> X) -> X -> X.
(* Examples (fun creates an anonymous function) *)
Definition zero : cnat := fun (X : Type) (f : X -> X) (x : X) => x.
Definition one : cnat := fun (X : Type) (f : X -> X) (x : X) => f x.
Definition two : cnat := fun (X : Type) (f : X -> X) (x : X) => f (f x).
(* Arithmetic *)
Definition succ (n : cnat) : cnat := fun (X : Type) (f : X -> X) (x : X) => f (n X f x).
Definition plus (n m : cnat) : cnat := fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).
Definition mult (n m : cnat) : cnat := fun (X : Type) (f : X -> X) (x : X) => n X (m X f) x.
Definition exp (n m : cnat) : cnat := fun (X : Type) (f : X -> X) (x : X) => (m (X -> X) (n X) f) x.