michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/pp): pretty printer was ignoring notation decls in the local scope

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-18 18:00:37 -08:00
parent 79fa6e4940
commit 8cfe5cf9ed
2 changed files with 36 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
examples/lean/ex5.lean
View file

@ -1,11 +1,11 @@
Push Push
Theorem ReflIf (A : Type) Theorem ReflIf (A : Type)
(R : A -> A -> Bool) (R : A → A → Bool)
(Symmetry : Pi x y, R x y -> R y x) (Symmetry : Π x y, R x y → R y x)
(Transitivity : Pi x y z, R x y -> R y z -> R x z) (Transitivity : Π x y z, R x y → R y z → R x z)
(Linked : Pi x, exists y, R x y) (Linked : Π x, ∃ y, R x y)
: :
Pi x, R x x := Π x, R x x :=
fun x, ExistsElim (Linked x) fun x, ExistsElim (Linked x)
(fun (w : A) (H : R x w), (fun (w : A) (H : R x w),
let L1 : R w x := Symmetry x w H let L1 : R w x := Symmetry x w H
@ -14,29 +14,49 @@ Pop
Push 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) Theorem ReflIf (A : Type)
(R : A -> A -> Bool) (R : A → A → Bool)
(Symmetry : forall x y, R x y => R y x) (Symmetry : ∀ x y, R x y ⇒ R y x)
(Transitivity : forall x y z, R x y => R y z => R x z) (Transitivity : ∀ x y z, R x y ⇒ R y z ⇒ R x z)
(Linked : forall x, exists y, R x y) (Linked : ∀ x, ∃ y, R x y)
: :
forall x, R x x := ∀ x, R x x :=
ForallIntro (fun x, ForallIntro (fun x,
ExistsElim (ForallElim Linked x) ExistsElim (ForallElim Linked x)
(fun (w : A) (H : R x w), (fun (w : A) (H : R x w),
let L1 : R w x := (MP (ForallElim (ForallElim Symmetry x) w) H) let L1 : R w x := (MP (ForallElim (ForallElim Symmetry x) w) H)
in (MP (MP (ForallElim (ForallElim (ForallElim Transitivity x) w) x) H) L1))) 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 Pop
Scope Scope
(* Same example again. *) (* Same example again. *)
Variable A : Type Variable A : Type
Variable R : A -> A -> Bool Variable R : A → A → Bool
Axiom Symmetry {x y : A} : R x y -> R y x 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 Transitivity {x y z : A} : R x y → R y z → R x z
Axiom Linked (x : A) : exists y, R x y Axiom Linked (x : A) : ∃ y, R x y
Theorem ReflIf (x : A) : R x x := Theorem ReflIf (x : A) : R x x :=
ExistsElim (Linked x) (fun (w : A) (H : R x w), ExistsElim (Linked x) (fun (w : A) (H : R x w),

1
src/frontends/lean/parser.cpp
View file

@ -2085,6 +2085,7 @@ class parser::imp {
m_env = env; m_env = env;
m_elaborator.reset(env); m_elaborator.reset(env);
m_type_inferer.reset(env); m_type_inferer.reset(env);
m_io_state.set_formatter(mk_pp_formatter(env));
} }
void parse_scope() { void parse_scope() {