16 lines
387 B
Text
16 lines
387 B
Text
|
let flip
|
||
|
|
: ∀(A : Type) → ∀(B : Type) → ∀(C : Type) → (B → A → C) → A → B → C
|
||
|
|
= λ(A : Type) →
|
||
|
|
λ(B : Type) →
|
||
|
|
λ(C : Type) →
|
||
|
|
λ(f : B → A → C) →
|
||
|
|
λ(a : A) →
|
||
|
|
λ(b : B) →
|
||
|
|
f b a
|
||
|
|
|
||
|
|
let example1 =
|
||
|
|
assert
|
||
|
|
: flip Text Text Text (λ(a : Text) → λ(b : Text) → a ++ b) "a" "b" ≡ "ba"
|
||
|
|
|
||
|
|
in flip
|