22 lines
486 B
Text
22 lines
486 B
Text
|
λ(nix : ../NixPrelude.dhall) →
|
||
|
let add = ./add.dhall nix
|
||
|
|
||
|
let negate = ./negate.dhall nix
|
||
|
|
||
|
let divide = ./divide.dhall nix
|
||
|
|
||
|
let succ = λ(n : Double) → add n 1.0
|
||
|
|
||
|
let build =
|
||
|
λ ( builder
|
||
|
: ∀(double : Type) →
|
||
|
(double → double) →
|
||
|
(double → double) →
|
||
|
(double → double → double) →
|
||
|
double →
|
||
|
double
|
||
|
) →
|
||
|
builder Double succ negate divide 0.0
|
||
|
|
||
|
in build
|