From 8cfe5cf9edc02f1724117e2fb3c507b353f36dbb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Dec 2013 18:00:37 -0800
Subject: [PATCH] fix(frontends/lean/pp): pretty printer was ignoring notation
 decls in the local scope

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/lean/ex5.lean        | 50 ++++++++++++++++++++++++-----------
 src/frontends/lean/parser.cpp |  1 +
 2 files changed, 36 insertions(+), 15 deletions(-)

diff --git a/examples/lean/ex5.lean b/examples/lean/ex5.lean
index 5f03e44f3..ede87c208 100644
--- a/examples/lean/ex5.lean
+++ b/examples/lean/ex5.lean
@@ -1,11 +1,11 @@
 Push
    Theorem ReflIf (A : Type)
-                  (R : A -> A -> Bool)
-                  (Symmetry : Pi x y, R x y -> R y x)
-                  (Transitivity : Pi x y z, R x y -> R y z -> R x z)
-                  (Linked : Pi x, exists y, R x y)
+                  (R : A → A → Bool)
+                  (Symmetry : Π x y, R x y → R y x)
+                  (Transitivity : Π x y z, R x y → R y z → R x z)
+                  (Linked : Π x, ∃ y, R x y)
                   :
-                  Pi x, R x x :=
+                  Π x, R x x :=
        fun x, ExistsElim (Linked x)
              (fun (w : A) (H : R x w),
                  let L1 : R w x := Symmetry x w H
@@ -14,29 +14,49 @@ Pop
 
 Push
   (*
-    Same example but using forall instead of Pi and => instead of ->
+    Same example but using ∀ instead of Π and ⇒ instead of →
   *)
   Theorem ReflIf (A : Type)
-                 (R : A -> A -> Bool)
-                 (Symmetry : forall x y, R x y => R y x)
-                 (Transitivity : forall x y z, R x y => R y z => R x z)
-                 (Linked : forall x, exists y, R x y)
+                 (R : A → A → Bool)
+                 (Symmetry : ∀ x y, R x y ⇒ R y x)
+                 (Transitivity : ∀ x y z, R x y ⇒ R y z ⇒ R x z)
+                 (Linked : ∀ x, ∃ y, R x y)
                  :
-                 forall x, R x x :=
+                 ∀ x, R x x :=
     ForallIntro (fun x,
          ExistsElim (ForallElim Linked x)
             (fun (w : A) (H : R x w),
                 let L1 : R w x := (MP (ForallElim (ForallElim Symmetry x) w) H)
                 in (MP (MP (ForallElim (ForallElim (ForallElim Transitivity x) w) x) H) L1)))
+
+    (* We can make the previous example less verbose by using custom notation *)
+
+    Infixl 50 !  : ForallElim
+    Infixl 30 << : MP
+
+    Theorem ReflIf2 (A : Type)
+                    (R : A → A → Bool)
+                    (Symmetry : ∀ x y, R x y ⇒ R y x)
+                    (Transitivity : ∀ x y z, R x y ⇒ R y z ⇒ R x z)
+                    (Linked : ∀ x, ∃ y, R x y)
+                    :
+                    ∀ x, R x x :=
+       ForallIntro (fun x,
+          ExistsElim (Linked ! x)
+             (fun (w : A) (H : R x w),
+                  let L1 : R w x := Symmetry ! x ! w << H
+                  in Transitivity ! x ! w ! x << H << L1))
+
+    Show Environment 1
 Pop
 
 Scope
   (* Same example again. *)
   Variable A : Type
-  Variable R : A -> A -> Bool
-  Axiom Symmetry  {x y : A} : R x y -> R y x
-  Axiom Transitivity {x y z : A} : R x y -> R y z -> R x z
-  Axiom Linked (x : A) : exists y, R x y
+  Variable R : A → A → Bool
+  Axiom Symmetry  {x y : A} : R x y → R y x
+  Axiom Transitivity {x y z : A} : R x y → R y z → R x z
+  Axiom Linked (x : A) : ∃ y, R x y
 
   Theorem ReflIf (x : A) : R x x :=
       ExistsElim (Linked x) (fun (w : A) (H : R x w),
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index f391b7893..d47f4ff4d 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2085,6 +2085,7 @@ class parser::imp {
         m_env = env;
         m_elaborator.reset(env);
         m_type_inferer.reset(env);
+        m_io_state.set_formatter(mk_pp_formatter(env));
     }
 
     void parse_scope() {