17 lines
418 B
Text
17 lines
418 B
Text
|
λ(nix : ../NixPrelude.dhall) →
|
||
|
|
let Any/toAny = ../Any/toAny.dhall nix
|
||
|
|
|
||
|
|
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||
|
|
|
||
|
|
let seq
|
||
|
|
: ∀(A : Type) → ∀(B : Type) → A → B → B
|
||
|
|
= λ(A : Type) →
|
||
|
|
λ(B : Type) →
|
||
|
|
λ(a : A) →
|
||
|
|
λ(b : B) →
|
||
|
|
Any/toTypeUnchecked
|
||
|
|
B
|
||
|
|
(nix.builtins.seq (Any/toAny A a) (Any/toAny B b))
|
||
|
|
|
||
|
|
in seq
|