From 0a08494f4df0b53043359990d150d8f7a5f96a46 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Sep 2013 23:21:43 -0700 Subject: [PATCH] Add another bad example for current elaborator Signed-off-by: Leonardo de Moura --- tests/lean/bad/t5.lean | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 tests/lean/bad/t5.lean diff --git a/tests/lean/bad/t5.lean b/tests/lean/bad/t5.lean new file mode 100644 index 000000000..0e0d50d1b --- /dev/null +++ b/tests/lean/bad/t5.lean @@ -0,0 +1,27 @@ +Variable g {A : Type} (a : A) : A +Variable a : Int +Variable b : Int +Axiom H1 : a = b +(* +The following axiom fails to be elaborated because: +1- (g a) is actually (g _ a) +2- > is overloaded notation for Nat::gt, Int::gt and Real::gt +3- The current elaborator selects one of the overloads before + the hole in (g _ a) is solved. Thus, it selects Nat::gt. +4- During elaboration, we transform (g _ a) into (g Int a), + and a type error is detected. + +The next elaborator should address this problem. +*) +Axiom H2 : (g a) > 0 + +(* +A possible workaround is to manually add the coercion in 0. +The coercion is called nat_to_int. We define the notation +_ i to make it easier to write +*) +Notation 100 _ i : nat_to_int +Axiom H2 : (g a) > 0i + +Theorem T1 : (g b) > 0i := Subst (λ x, (g x) > 0i) H2 H1 +Show Environment 2