-- one could define the naturals as follows
type Nat
  | zero : Nat
  | succ : Nat → Nat

-- which will bring a recursor for the type into scope
-- rec[Nat] : A → (A → A) → Nat → A


-- defining addition as
add : Nat → Nat → Nat
 := rec[Nat] (λx. x) (λf n. succ (f n))

-- since                | rec[Nat] : A → (A → A) → Nat → A
-- which generalizes to | rec[Nat] : (Nat → Nat) → ((Nat → Nat) → (Nat → Nat)) → Nat → (Nat → Nat)
--                                   ^ adding 0    ^ recursively adding one more       ^ resulting addition type

-- id is used to not add anything, the second function takes the last addition function and adds a layer
-- of succ onto it, this way it generates a function for adding the right amount.



-- multiplication is defined similairly
mul : Nat → Nat → Nat
 := rec[Nat] (λx. zero) (λf n. add n (f n))



-- here's an example of a simpler type
type Bool
  | true : Bool
  | false : Bool

not : Bool → Bool
 := rec[Bool] false true

-- now, let's look at a bit more interesting example
type Expr
  | ENat : Nat →  Expr
  | EAdd : Expr → Expr → Expr
  | EMul : Expr → Expr → Expr

-- this generates the following recursor
-- rec[Expr] : (Nat → A) → (A → A → A) → (A → A → A) → Expr → A



eval : Expr → Nat
 := rec[Expr] (λx. x) add mul

-- here's some other functions
isEven : Nat → Bool
 := rec[Nat] true not

type bot

absurd : bot -> A
  := rec[bot]

id : A -> A
 := λx. x