26 lines
630 B
Text
26 lines
630 B
Text
let Integer/add = ./add.dhall
|
|
|
|
let negate = ./negate.dhall
|
|
|
|
let Integer/succ
|
|
: Integer → Integer
|
|
= λ(n : Integer) → Integer/add n +1
|
|
|
|
let build
|
|
: ( ∀(integer : Type) →
|
|
∀(succ : integer → integer) →
|
|
∀(negate : integer → integer) →
|
|
∀(zero : integer) →
|
|
integer
|
|
) →
|
|
Integer
|
|
= λ ( builder
|
|
: ∀(integer : Type) →
|
|
∀(succ : integer → integer) →
|
|
∀(negate : integer → integer) →
|
|
∀(zero : integer) →
|
|
integer
|
|
) →
|
|
builder Integer Integer/succ negate +0
|
|
|
|
in build
|