lean2/tests/lean/let1.lean.expected.out
Leonardo de Moura 5f360cd8ec feat(kernel/error_msgs): improve application type mismatch error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 07:08:12 -07:00

38 lines
1.9 KiB
Text

let and_intro : ∀ (p q : Prop),
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q :=
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
H H1 H2,
and_elim_left : ∀ (p q : Prop),
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
H p (λ (H1 : p) (H2 : q), H1),
and_elim_right : ∀ (p q : Prop),
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
H q (λ (H1 : p) (H2 : q), H2)
in and_intro :
∀ (p q : Prop),
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q
let1.lean:16:10: error: type mismatch at application
let and_intro : ∀ (p q : Prop),
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p :=
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
H H1 H2,
and_elim_left : ∀ (p q : Prop),
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
H p (λ (H1 : p) (H2 : q), H1),
and_elim_right : ∀ (p q : Prop),
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
H q (λ (H1 : p) (H2 : q), H2)
in and_intro
term
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
H H1 H2
is expected of type
∀ (p q : Prop),
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p
but is given type
∀ (p q : Prop),
p → q → (∀ (c : Prop), (p → q → c) → c)