From 873a5c8605162946bd65e1e41e14904e3488b04f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jun 2014 14:11:26 -0700 Subject: [PATCH] test(lean): add 'let' expression test Signed-off-by: Leonardo de Moura --- tests/lean/let1.lean | 23 +++++++++++++++++++++++ tests/lean/let1.lean.expected.out | 5 +++++ 2 files changed, 28 insertions(+) create mode 100644 tests/lean/let1.lean create mode 100644 tests/lean/let1.lean.expected.out diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean new file mode 100644 index 000000000..86c1f325f --- /dev/null +++ b/tests/lean/let1.lean @@ -0,0 +1,23 @@ +-- Correct version +check let bool : Type.{1} := Type.{0}, + and (p q : bool) : bool := ∀ c : bool, (p → q → c) → c, + infixl `∧` 25 := and, + and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q + := λ (c : bool) (H : p → q → c), H H1 H2, + and_elim_left (p q : bool) (H : p ∧ q) : p + := H p (λ (H1 : p) (H2 : q), H1), + and_elim_right (p q : bool) (H : p ∧ q) : q + := H q (λ (H1 : p) (H2 : q), H2) + in and_intro + +check let bool : Type.{1} := Type.{0}, + and (p q : bool) : bool := ∀ c : bool, (p → q → c) → c, + infixl `∧` 25 := and, + and_intro (p q : bool) (H1 : p) (H2 : q) : q ∧ p + := λ (c : bool) (H : p → q → c), H H1 H2, + and_elim_left (p q : bool) (H : p ∧ q) : p + := H p (λ (H1 : p) (H2 : q), H1), + and_elim_right (p q : bool) (H : p ∧ q) : q + := H q (λ (H1 : p) (H2 : q), H2) + in and_intro + diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out new file mode 100644 index 000000000..8116c8b37 --- /dev/null +++ b/tests/lean/let1.lean.expected.out @@ -0,0 +1,5 @@ +let bool : Type := Bool in (let and : bool -> bool -> bool := fun (p : bool) (q : bool), (Pi (c : bool) (a : p -> q -> c), c) in (let and_intro : Pi (p : bool) (q : bool) (H1 : p) (H2 : q), (and p q) := fun (p : bool) (q : bool) (H1 : p) (H2 : q) (c : bool) (H : p -> q -> c), (H H1 H2) in (let and_elim_left : Pi (p : bool) (q : bool) (H : and p q), p := fun (p : bool) (q : bool) (H : and p q), (H p (fun (H1 : p) (H2 : q), H1)) in (let and_elim_right : Pi (p : bool) (q : bool) (H : and p q), q := fun (p : bool) (q : bool) (H : and p q), (H q (fun (H1 : p) (H2 : q), H2)) in and_intro)))) : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), c +let1.lean:16:10: error: type mismatch at definition 'and_intro', expected type + Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) q p) +given type: + Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), c