From 49a6048060de2e267128d08f30252745719926c9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Jun 2014 13:18:32 -0700 Subject: [PATCH] test(lean/run): add another test for new elaborator Signed-off-by: Leonardo de Moura --- tests/lean/run/e3.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/lean/run/e3.lean diff --git a/tests/lean/run/e3.lean b/tests/lean/run/e3.lean new file mode 100644 index 000000000..4002c5ab1 --- /dev/null +++ b/tests/lean/run/e3.lean @@ -0,0 +1,21 @@ +definition Bool [inline] := Type.{0} + +definition false := ∀x : Bool, x +check false + +theorem false_elim (C : Bool) (H : false) : C +:= H C + +definition eq {A : Type} (a b : A) +:= ∀ {P : A → Bool}, P a → P b + +check eq + +infix `=` 50 := eq + +theorem refl {A : Type} (a : A) : a = a +:= λ P H, H + +theorem subst {A : Type} {P : A -> Bool} {a b : A} (H1 : a = b) (H2 : P a) : P b +:= @H1 P H2 +