lean2/tests/lean/let1.lean.expected.out

16 lines
426 B
Text
Raw Permalink Normal View History

let bool := Prop,
and := λ p q, Π c, (p → q → c) → c,
and_intro := λ p q H1 H2 c H, H H1 H2
in and_intro :
∀ p q,
p → q → (∀ c, (p → q → c) → c)
let1.lean:19:19: error: type mismatch at term
λ p q H1 H2 c H,
H H1 H2
has type
∀ p q,
p → q → (∀ c, (p → q → c) → c)
but is expected to have type
∀ p q,
p → q → (λ p q, ∀ c, (p → q → c) → c) q p