From bc92671ae46628c84a8528d6c641510a4921bfaa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Oct 2013 17:12:50 -0700
Subject: [PATCH] fix(frontends/lean/notation): adjust the implicit arguments
 of TransExt, and add new test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/notation.cpp  |  2 +-
 tests/lean/eq3.lean              | 12 ++++++++++++
 tests/lean/eq3.lean.expected.out | 12 ++++++++++++
 3 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/eq3.lean
 create mode 100644 tests/lean/eq3.lean.expected.out

diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
index 6dde7d299..5466161bc 100644
--- a/src/frontends/lean/notation.cpp
+++ b/src/frontends/lean/notation.cpp
@@ -81,6 +81,7 @@ void init_builtin_notation(frontend & f) {
     f.mark_implicit_arguments(mk_discharge_fn(), {true, true, false});
     f.mark_implicit_arguments(mk_refl_fn(), {true, false});
     f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, false, false, false});
+    f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, true, false, false});
     f.mark_implicit_arguments(mk_eta_fn(), {true, true, false});
     f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false});
     f.mark_implicit_arguments(mk_dom_inj_fn(), {true, true, true, true, false});
@@ -102,7 +103,6 @@ void init_builtin_notation(frontend & f) {
     f.mark_implicit_arguments(mk_disj_cases_fn(), {true, true, true, false, false, false});
     f.mark_implicit_arguments(mk_symm_fn(), {true, true, true, false});
     f.mark_implicit_arguments(mk_trans_fn(), {true, true, true, true, false, false});
-    f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, false, false});
     f.mark_implicit_arguments(mk_eqt_elim_fn(), {true, false});
     f.mark_implicit_arguments(mk_eqt_intro_fn(), {true, false});
     f.mark_implicit_arguments(mk_congr1_fn(), {true, true, true, true, false, false});
diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean
new file mode 100644
index 000000000..3d840ea79
--- /dev/null
+++ b/tests/lean/eq3.lean
@@ -0,0 +1,12 @@
+
+
+Variable Vector : Nat -> Type
+Variable n  : Nat
+Variable v1 : Vector n
+Variable v2 : Vector (n + 0)
+Variable v3 : Vector (0 + n)
+Axiom H1 : v1 == v2
+Axiom H2 : v2 == v3
+Check TransExt H1 H2
+Set pp::implicit true
+Check TransExt H1 H2
diff --git a/tests/lean/eq3.lean.expected.out b/tests/lean/eq3.lean.expected.out
new file mode 100644
index 000000000..1707daa8c
--- /dev/null
+++ b/tests/lean/eq3.lean.expected.out
@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: Vector
+  Assumed: n
+  Assumed: v1
+  Assumed: v2
+  Assumed: v3
+  Assumed: H1
+  Assumed: H2
+TransExt H1 H2 : v1 == v3
+  Set: lean::pp::implicit
+TransExt::explicit (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3