30 lines
958 B
Text
30 lines
958 B
Text
let Integer/add =
|
|
https://raw.githubusercontent.com/dhall-lang/dhall-lang/v22.0.0/Prelude/Integer/add.dhall
|
|
sha256:7da1306a0bf87c5668beead2a1db1b18861e53d7ce1f38057b2964b649f59c3b
|
|
|
|
let negate =
|
|
https://raw.githubusercontent.com/dhall-lang/dhall-lang/v22.0.0/Prelude/Integer/negate.dhall
|
|
sha256:2373c992e1de93634bc6a8781eb073b2a92a70170133e49762a785f3a136df5d
|
|
|
|
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
|