35 lines
1.1 KiB
Text
35 lines
1.1 KiB
Text
|
λ(nix : ../NixPrelude.dhall) →
|
||
|
|
let Any = ../Any/Type.dhall
|
||
|
|
|
||
|
|
let Any/toAny = ../Any/toAny.dhall nix
|
||
|
|
|
||
|
|
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||
|
|
|
||
|
|
let Any/equal = ../Any/equal.dhall nix
|
||
|
|
|
||
|
|
in λ(t : Type) →
|
||
|
|
let FunctionType = λ(x : Type) → x → (t → t) → t → t
|
||
|
|
|
||
|
|
let function =
|
||
|
|
λ(function : FunctionType Any) →
|
||
|
|
let functionArgs =
|
||
|
|
Any/toTypeUnchecked
|
||
|
|
(FunctionType (FunctionType Any))
|
||
|
|
(Any/toAny (FunctionType Any) function)
|
||
|
|
function
|
||
|
|
|
||
|
|
in λ(f : t → t) →
|
||
|
|
λ(x : t) →
|
||
|
|
let xp = f x
|
||
|
|
|
||
|
|
in if Any/equal (Any/toAny t xp) (Any/toAny t x)
|
||
|
|
then x
|
||
|
|
else functionArgs f xp
|
||
|
|
|
||
|
|
let functionErased =
|
||
|
|
Any/toTypeUnchecked
|
||
|
|
(FunctionType Any)
|
||
|
|
(Any/toAny (FunctionType (FunctionType Any)) function)
|
||
|
|
|
||
|
|
in function functionErased
|