25 lines
901 B
Text
25 lines
901 B
Text
let Integer/negative =
|
|
https://raw.githubusercontent.com/dhall-lang/dhall-lang/v22.0.0/Prelude/Integer/negative.dhall
|
|
sha256:23e4b3c61eea9e878a7f83bf25fd0ea2c6a6d60174890d65be885828b690a570
|
|
|
|
let Integer/abs =
|
|
https://raw.githubusercontent.com/dhall-lang/dhall-lang/v22.0.0/Prelude/Integer/abs.dhall
|
|
sha256:35212fcbe1e60cb95b033a4a9c6e45befca4a298aa9919915999d09e69ddced1
|
|
|
|
let fold
|
|
: Integer →
|
|
∀(integer : Type) →
|
|
∀(succ : integer → integer) →
|
|
∀(negate : integer → integer) →
|
|
∀(zero : integer) →
|
|
integer
|
|
= λ(e : Integer) →
|
|
λ(integer : Type) →
|
|
λ(succ : integer → integer) →
|
|
λ(negate : integer → integer) →
|
|
λ(zero : integer) →
|
|
let folded = Natural/fold (Integer/abs e) integer succ zero
|
|
|
|
in if Integer/negative e then negate folded else folded
|
|
|
|
in fold
|