From 028a9bd9bdddacff6bc10c04c94c682909222eb0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2014 08:52:46 -0800 Subject: [PATCH] feat(frontends/lean/scanner): use Lua style comments in Lean Signed-off-by: Leonardo de Moura --- doc/lean/expr.md | 2 - examples/lean/even.lean | 100 ++++++++++++--------------- examples/lean/ex1.lean | 14 ++-- examples/lean/ex3.lean | 24 +++---- examples/lean/ex4.lean | 6 +- examples/lean/ex5.lean | 18 ++--- examples/lean/set.lean | 2 +- examples/lean/tactic1.lean | 72 +++++++++---------- examples/lean/tactic_in_lua.lean | 2 +- src/builtin/cast.lean | 27 +++----- src/builtin/kernel.lean | 45 +++++------- src/frontends/lean/scanner.cpp | 21 +++++- src/frontends/lean/scanner.h | 1 + src/tests/frontends/lean/parser.cpp | 4 +- src/tests/frontends/lean/scanner.cpp | 7 +- tests/lean/arith7.lean | 9 ++- tests/lean/cast1.lean | 18 ++--- tests/lean/cast1.lean.expected.out | 2 +- tests/lean/config.lean | 2 +- tests/lean/ex2.lean | 3 +- tests/lean/ex2.lean.expected.out | 8 +-- tests/lean/implicit1.lean | 10 ++- tests/lean/implicit7.lean | 6 -- tests/lean/interactive/config.lean | 2 +- tests/lean/interactive/t12.lean | 54 +++++---------- tests/lean/let2.lean | 3 +- tests/lean/push.lean | 6 +- tests/lean/single.lean | 2 +- tests/lean/slow/config.lean | 2 +- tests/lean/tactic2.lean | 8 +-- tests/lean/tactic3.lean | 2 +- tests/lean/tst1.lean | 2 +- tests/lean/tst10.lean | 8 +-- tests/lean/tst6.lean | 10 +-- tests/lean/tst7.lean | 2 +- tests/lean/tst7.lean.expected.out | 2 +- tests/lua/coercion_bug1.lua | 8 +-- tests/lua/front.lua | 4 +- 38 files changed, 226 insertions(+), 292 deletions(-) diff --git a/doc/lean/expr.md b/doc/lean/expr.md index 6da57e98f..c52a254cf 100644 --- a/doc/lean/expr.md +++ b/doc/lean/expr.md @@ -111,5 +111,3 @@ SetOption pp::implicit false. SetOption pp::notation true. Check 1 = 2. ``` - -Note that, like the SML programming language, `(* comment *)` is a comment. diff --git a/examples/lean/even.lean b/examples/lean/even.lean index ef54a43af..51cb82cb1 100644 --- a/examples/lean/even.lean +++ b/examples/lean/even.lean @@ -1,37 +1,33 @@ Import macros. -(* -In this example, we prove two simple theorems about even/odd numbers. -First, we define the predicates even and odd. -*) +-- In this example, we prove two simple theorems about even/odd numbers. +-- First, we define the predicates even and odd. Definition even (a : Nat) := ∃ b, a = 2*b. Definition odd (a : Nat) := ∃ b, a = 2*b + 1. -(* - Prove that the sum of two even numbers is even. - - Notes: we use the macro - Obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2 - - It is syntax sugar for existential elimination. - It expands to - - ExistsElim [expr]_1 (fun [binding], [expr]_2) - - It is defined in the file macros.lua. - - We also use the calculational proof style. - See doc/lean/calc.md for more information. - - We use the first two Obtain-expressions to extract the - witnesses w1 and w2 s.t. a = 2*w1 and b = 2*w2. - We can do that because H1 and H2 are evidence/proof for the - fact that 'a' and 'b' are even. - - We use a calculational proof 'calc' expression to derive - the witness w1+w2 for the fact that a+b is also even. - That is, we provide a derivation showing that a+b = 2*(w1 + w2) -*) +-- Prove that the sum of two even numbers is even. +-- +-- Notes: we use the macro +-- Obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2 +-- +-- It is syntax sugar for existential elimination. +-- It expands to +-- +-- ExistsElim [expr]_1 (fun [binding], [expr]_2) +-- +-- It is defined in the file macros.lua. +-- +-- We also use the calculational proof style. +-- See doc/lean/calc.md for more information. +-- +-- We use the first two Obtain-expressions to extract the +-- witnesses w1 and w2 s.t. a = 2*w1 and b = 2*w2. +-- We can do that because H1 and H2 are evidence/proof for the +-- fact that 'a' and 'b' are even. +-- +-- We use a calculational proof 'calc' expression to derive +-- the witness w1+w2 for the fact that a+b is also even. +-- That is, we provide a derivation showing that a+b = 2*(w1 + w2) Theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b) := Obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1, Obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2, @@ -40,21 +36,19 @@ Theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b) ... = 2*w1 + 2*w2 : { Hw2 } ... = 2*(w1 + w2) : Symm (Nat::Distribute 2 w1 w2)). -(* - In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute. - Lean can infer them automatically. - - Refl is the reflexivity proof. (Refl a) is a proof that two - definitionally equal terms are indeed equal. - "Definitionally equal" means that they have the same normal form. - We can also view it as "Proof by computation". - The normal form of (1+1), and 2*1 is 2. - - Another remark: '2*w + 1 + 1' is not definitionally equal to '2*w + 2*1'. - The gotcha is that '2*w + 1 + 1' is actually '(2*w + 1) + 1' since + - is left associative. Moreover, Lean normalizer does not use - any theorems such as + associativity. -*) +-- In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute. +-- Lean can infer them automatically. +-- +-- Refl is the reflexivity proof. (Refl a) is a proof that two +-- definitionally equal terms are indeed equal. +-- "Definitionally equal" means that they have the same normal form. +-- We can also view it as "Proof by computation". +-- The normal form of (1+1), and 2*1 is 2. +-- +-- Another remark: '2*w + 1 + 1' is not definitionally equal to '2*w + 2*1'. +-- The gotcha is that '2*w + 1 + 1' is actually '(2*w + 1) + 1' since + +-- is left associative. Moreover, Lean normalizer does not use +-- any theorems such as + associativity. Theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1) := Obtain (w : Nat) (Hw : a = 2*w + 1), from H, ExistsIntro (w + 1) @@ -63,21 +57,15 @@ Theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1) ... = 2*w + 2*1 : Refl _ ... = 2*(w + 1) : Symm (Nat::Distribute _ _ _)). -(* - The following command displays the proof object produced by Lean after - expanding macros, and infering implicit/missing arguments. -*) +-- The following command displays the proof object produced by Lean after +-- expanding macros, and infering implicit/missing arguments. Show Environment 2. -(* - By default, Lean does not display implicit arguments. - The following command will force it to display them. -*) +-- By default, Lean does not display implicit arguments. +-- The following command will force it to display them. SetOption pp::implicit true. Show Environment 2. -(* - As an exercise, prove that the sum of two odd numbers is even, - and other similar theorems. -*) +-- As an exercise, prove that the sum of two odd numbers is even, +-- and other similar theorems. diff --git a/examples/lean/ex1.lean b/examples/lean/ex1.lean index 244f44d9e..d20c2f47e 100644 --- a/examples/lean/ex1.lean +++ b/examples/lean/ex1.lean @@ -1,35 +1,35 @@ Variable N : Type Variable h : N -> N -> N -(* Specialize congruence theorem for h-applications *) +-- Specialize congruence theorem for h-applications Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2 -(* Declare some variables *) +-- Declare some variables Variable a : N Variable b : N Variable c : N Variable d : N Variable e : N -(* Add axioms stating facts about these variables *) +-- Add axioms stating facts about these variables Axiom H1 : (a = b ∧ b = c) ∨ (d = c ∧ a = d) Axiom H2 : b = e -(* Proof that (h a b) = (h c e) *) +-- Proof that (h a b) = (h c e) Theorem T1 : (h a b) = (h c e) := DisjCases H1 (λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2) (λ C2, CongrH (Trans (Conjunct2 C2) (Conjunct1 C2)) H2) -(* We can use theorem T1 to prove other theorems *) +-- We can use theorem T1 to prove other theorems Theorem T2 : (h a (h a b)) = (h a (h c e)) := CongrH (Refl a) T1 -(* Display the last two objects (i.e., theorems) added to the environment *) +-- Display the last two objects (i.e., theorems) added to the environment Show Environment 2 -(* Show implicit arguments *) +-- Show implicit arguments SetOption lean::pp::implicit true SetOption pp::width 150 Show Environment 2 diff --git a/examples/lean/ex3.lean b/examples/lean/ex3.lean index 5d4c60b0d..e0e0b1846 100644 --- a/examples/lean/ex3.lean +++ b/examples/lean/ex3.lean @@ -9,19 +9,17 @@ Theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a) (λ H_a, Disj2 b H_a) (λ H_b, Disj1 H_b a). -(* --------------------------------- -(EM a) is the excluded middle a ∨ ¬a -(MT H H_na) is Modus Tollens with - H : (a ⇒ b) ⇒ a) - H_na : ¬a -produces - ¬(a ⇒ b) - -NotImp1 applied to - (MT H H_na) : ¬(a ⇒ b) -produces - a ------------------------------------ *) +-- (EM a) is the excluded middle a ∨ ¬a +-- (MT H H_na) is Modus Tollens with +-- H : (a ⇒ b) ⇒ a) +-- H_na : ¬a +-- produces +-- ¬(a ⇒ b) +-- +-- NotImp1 applied to +-- (MT H H_na) : ¬(a ⇒ b) +-- produces +-- a Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a := Assume H, DisjCases (EM a) (λ H_a, H_a) diff --git a/examples/lean/ex4.lean b/examples/lean/ex4.lean index 6adb34bca..48521901d 100644 --- a/examples/lean/ex4.lean +++ b/examples/lean/ex4.lean @@ -1,8 +1,8 @@ Import Int Import tactic Definition a : Nat := 10 -(* Trivial indicates a "proof by evaluation" *) +-- Trivial indicates a "proof by evaluation" Theorem T1 : a > 0 := Trivial Theorem T2 : a - 5 > 3 := Trivial -(* The next one is commented because it fails *) -(* Theorem T3 : a > 11 := Trivial *) +-- The next one is commented because it fails +-- Theorem T3 : a > 11 := Trivial diff --git a/examples/lean/ex5.lean b/examples/lean/ex5.lean index ede87c208..9ca5217ae 100644 --- a/examples/lean/ex5.lean +++ b/examples/lean/ex5.lean @@ -13,9 +13,7 @@ Push Pop Push - (* - Same example but using ∀ instead of Π and ⇒ instead of → - *) + -- Same example but using ∀ instead of Π and ⇒ instead of → Theorem ReflIf (A : Type) (R : A → A → Bool) (Symmetry : ∀ x y, R x y ⇒ R y x) @@ -29,7 +27,7 @@ Push 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 *) + -- We can make the previous example less verbose by using custom notation Infixl 50 ! : ForallElim Infixl 30 << : MP @@ -51,7 +49,7 @@ Push Pop Scope - (* Same example again. *) + -- Same example again. Variable A : Type Variable R : A → A → Bool Axiom Symmetry {x y : A} : R x y → R y x @@ -63,15 +61,13 @@ Scope let L1 : R w x := Symmetry H in Transitivity H L1) - (* Even more compact proof of the same theorem *) + -- Even more compact proof of the same theorem Theorem ReflIf2 (x : A) : R x x := ExistsElim (Linked x) (fun w H, Transitivity H (Symmetry H)) -(* - The command EndScope exports both theorem to the main scope - The variables and axioms in the scope become parameters to both theorems. -*) + -- The command EndScope exports both theorem to the main scope + -- The variables and axioms in the scope become parameters to both theorems. EndScope -(* Display the last two theorems *) +-- Display the last two theorems Show Environment 2 \ No newline at end of file diff --git a/examples/lean/set.lean b/examples/lean/set.lean index fb0da8518..2c91d03da 100644 --- a/examples/lean/set.lean +++ b/examples/lean/set.lean @@ -31,7 +31,7 @@ Theorem SubsetAntiSymm (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 L2 : x ∈ s2 ⇒ x ∈ s1 := Instantiate H2 x in ImpAntisym L1 L2) -(* Compact (but less readable) version of the previous theorem *) +-- Compact (but less readable) version of the previous theorem Theorem SubsetAntiSymm2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := For s1 s2, Assume H1 H2, MP (Instantiate (SubsetExt A) s1 s2) diff --git a/examples/lean/tactic1.lean b/examples/lean/tactic1.lean index 7efa563eb..7a2c02b76 100644 --- a/examples/lean/tactic1.lean +++ b/examples/lean/tactic1.lean @@ -1,7 +1,5 @@ -(* -This example demonstrates how to specify a proof skeleton that contains -"holes" that must be filled using user-defined tactics. -*) +-- This example demonstrates how to specify a proof skeleton that contains +-- "holes" that must be filled using user-defined tactics. (** -- Import useful macros for creating tactics @@ -14,56 +12,48 @@ conj_hyp = conj_hyp_tac() conj = conj_tac() **) -(* -The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it. -The "hint" is a tactic that should be used to fill the "hole". -In the following example, we use the tactic "auto" defined by the Lua code above. - -The (show [expr] by [tactic]) expression is also creating a "hole" and associating a "hint" to it. -The expression [expr] after the shows is fixing the type of the "hole" -*) +-- The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it. +-- The "hint" is a tactic that should be used to fill the "hole". +-- In the following example, we use the tactic "auto" defined by the Lua code above. +-- +-- The (show [expr] by [tactic]) expression is also creating a "hole" and associating a "hint" to it. +-- The expression [expr] after the shows is fixing the type of the "hole" Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 : A := (by auto), lemma2 : B := (by auto) in (show B /\ A by auto) -Show Environment 1. (* Show proof for the previous theorem *) +Show Environment 1. -- Show proof for the previous theorem -(* -When hints are not provided, the user must fill the (remaining) holes using tactic command sequences. -Each hole must be filled with a tactic command sequence that terminates with the command 'done' and -successfully produces a proof term for filling the hole. Here is the same example without hints -This style is more convenient for interactive proofs -*) +-- When hints are not provided, the user must fill the (remaining) holes using tactic command sequences. +-- Each hole must be filled with a tactic command sequence that terminates with the command 'done' and +-- successfully produces a proof term for filling the hole. Here is the same example without hints +-- This style is more convenient for interactive proofs Theorem T2 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, - let lemma1 : A := _, (* first hole *) - lemma2 : B := _ (* second hole *) - in _. (* third hole *) - auto. done. (* tactic command sequence for the first hole *) - auto. done. (* tactic command sequence for the second hole *) - auto. done. (* tactic command sequence for the third hole *) + let lemma1 : A := _, -- first hole + lemma2 : B := _ -- second hole + in _. -- third hole + auto. done. -- tactic command sequence for the first hole + auto. done. -- tactic command sequence for the second hole + auto. done. -- tactic command sequence for the third hole -(* -In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics. -*) +-- In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics. Theorem T3 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, - let lemma1 : A := _, (* first hole *) - lemma2 : B := _ (* second hole *) - in _. (* third hole *) - conj_hyp. exact. done. (* tactic command sequence for the first hole *) - conj_hyp. exact. done. (* tactic command sequence for the second hole *) - conj. exact. done. (* tactic command sequence for the third hole *) + let lemma1 : A := _, -- first hole + lemma2 : B := _ -- second hole + in _. -- third hole + conj_hyp. exact. done. -- tactic command sequence for the first hole + conj_hyp. exact. done. -- tactic command sequence for the second hole + conj. exact. done. -- tactic command sequence for the third hole -(* -We can also mix the two styles (hints and command sequences) -*) +-- We can also mix the two styles (hints and command sequences) Theorem T4 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, - let lemma1 : A := _, (* first hole *) - lemma2 : B := _ (* second hole *) + let lemma1 : A := _, -- first hole + lemma2 : B := _ -- second hole in (show B /\ A by auto). - auto. done. (* tactic command sequence for the first hole *) - auto. done. (* tactic command sequence for the second hole *) + auto. done. -- tactic command sequence for the first hole + auto. done. -- tactic command sequence for the second hole diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean index d6770310d..c185fd22c 100644 --- a/examples/lean/tactic_in_lua.lean +++ b/examples/lean/tactic_in_lua.lean @@ -68,5 +68,5 @@ Theorem T (a b : Bool) : a => b => a /\ b := _. (** Then(Repeat(OrElse(imp_tac(), conj_in_lua)), assumption_tac()) **) done -(* Show proof created using our script *) +-- Show proof created using our script Show Environment 1. diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean index 409004750..c440b311f 100644 --- a/src/builtin/cast.lean +++ b/src/builtin/cast.lean @@ -1,35 +1,24 @@ -(* - "Type casting" library. -*) +-- "Type casting" library. -(* - The cast operator allows us to cast an element of type A - into B if we provide a proof that types A and B are equal. -*) +-- The cast operator allows us to cast an element of type A +-- into B if we provide a proof that types A and B are equal. Variable cast {A B : (Type U)} : A == B → A → B. -(* - The CastEq axiom states that for any cast of x is equal to x. -*) + +-- The CastEq axiom states that for any cast of x is equal to x. Axiom CastEq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x. -(* - The CastApp axiom "propagates" the cast over application -*) +-- The CastApp axiom "propagates" the cast over application Axiom CastApp {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} (H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : A == A') (f : Π x : A, B x) (x : A) : cast H1 f (cast H2 x) == f x. -(* - If two (dependent) function spaces are equal, then their domains are equal. -*) +-- If two (dependent) function spaces are equal, then their domains are equal. Axiom DomInj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} (H : (Π x : A, B x) == (Π x : A', B' x)) : A == A'. -(* - If two (dependent) function spaces are equal, then their ranges are equal. -*) +-- If two (dependent) function spaces are equal, then their ranges are equal. Axiom RanInj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} (H : (Π x : A, B x) == (Π x : A', B' x)) (a : A) : B a == B' (cast (DomInj H) a). diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 72f0d681d..9ed27dab6 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -4,7 +4,7 @@ Universe M : 512. Universe U : M+512. Variable Bool : Type. -(* The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions. *) +-- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions. Builtin true : Bool. Builtin false : Bool. Builtin if {A : (Type U)} : Bool → A → A → A. @@ -43,12 +43,11 @@ Infixr 35 && : and. Infixr 35 /\ : and. Infixr 35 ∧ : and. -(* Forall is a macro for the identifier forall, we use that - because the Lean parser has the builtin syntax sugar: - forall x : T, P x - for - (forall T (fun x : T, P x)) -*) +-- Forall is a macro for the identifier forall, we use that +-- because the Lean parser has the builtin syntax sugar: +-- forall x : T, P x +-- for +-- (forall T (fun x : T, P x)) Definition Forall (A : TypeU) (P : A → Bool) : Bool := P == (λ x : A, true). @@ -106,7 +105,7 @@ Theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false Theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b := Subst H2 H1. -(* Assume is a 'macro' that expands into a Discharge *) +-- Assume is a 'macro' that expands into a Discharge Theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c := Assume Ha, MP H2 (MP H1 Ha). @@ -142,7 +141,7 @@ Theorem NotImp2 {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b := Assume H1 : b, Absurd (show a ⇒ b, Assume H2 : a, H1) (show ¬ (a ⇒ b), H). -(* Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean *) +-- Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean Theorem Conj {a b : Bool} (H1 : a) (H2 : b) : a ∧ b := Assume H : a ⇒ ¬ b, Absurd H2 (MP H H1). @@ -153,7 +152,7 @@ Theorem Conjunct1 {a b : Bool} (H : a ∧ b) : a Theorem Conjunct2 {a b : Bool} (H : a ∧ b) : b := DoubleNegElim (NotImp2 H). -(* Remark: disjunction is defined as ¬ a ⇒ b in Lean *) +-- Remark: disjunction is defined as ¬ a ⇒ b in Lean Theorem Disj1 {a : Bool} (H : a) (b : Bool) : a ∨ b := Assume H1 : ¬ a, AbsurdElim b H H1. @@ -201,19 +200,15 @@ Theorem EqTIntro {a : Bool} (H : a) : a == true Theorem Congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a := SubstP (fun h : (Π x : A, B x), f a == h a) (Refl (f a)) H. -(* -Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b) -are not "definitionally equal". They are (B a) and (B b). -They are provably equal, we just have to apply Congr1. -*) +-- Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b) +-- are not "definitionally equal". They are (B a) and (B b). +-- They are provably equal, we just have to apply Congr1. Theorem Congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b := SubstP (fun x : A, f a == f x) (Refl (f a)) H. -(* -Remark: like the previous theorem we use heterogeneous equality. We cannot use Trans theorem -because the types are not definitionally equal. -*) +-- Remark: like the previous theorem we use heterogeneous equality. We cannot use Trans theorem +-- because the types are not definitionally equal. Theorem Congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b := HTrans (Congr2 f H2) (Congr1 b H1). @@ -225,7 +220,7 @@ Theorem ForallIntro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A := Trans (Symm (Eta P)) (Abst (λ x, EqTIntro (H x))). -(* Remark: the existential is defined as (¬ (forall x : A, ¬ P x)) *) +-- Remark: the existential is defined as (¬ (forall x : A, ¬ P x)) Theorem ExistsElim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : Π (a : A) (H : P a), B) : B := Refute (λ R : ¬ B, @@ -236,12 +231,10 @@ Theorem ExistsIntro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P := Assume H1 : (∀ x : A, ¬ P x), Absurd H (ForallElim H1 a). -(* -At this point, we have proved the theorems we need using the -definitions of forall, exists, and, or, =>, not. We mark (some of) -them as opaque. Opaque definitions improve performance, and -effectiveness of Lean's elaborator. -*) +-- At this point, we have proved the theorems we need using the +-- definitions of forall, exists, and, or, =>, not. We mark (some of) +-- them as opaque. Opaque definitions improve performance, and +-- effectiveness of Lean's elaborator. SetOpaque implies true. SetOpaque not true. diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 04ce7e830..81bef0df1 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -165,6 +165,20 @@ void scanner::read_comment() { } } +void scanner::read_single_line_comment() { + while (true) { + if (curr() == '\n') { + new_line(); + next(); + return; + } else if (curr() == EOF) { + return; + } else { + next(); + } + } +} + bool scanner::is_command(name const & n) const { return std::any_of(m_commands.begin(), m_commands.end(), [&](name const & c) { return c == n; }); } @@ -431,7 +445,7 @@ scanner::token scanner::scan() { next(); return read_script_block(); } else { - read_comment(); + throw_exception("old comment style"); break; } } else { @@ -447,7 +461,10 @@ scanner::token scanner::scan() { next(); if (normalize(curr()) == '0') { return read_number(false); - } else if (normalize(curr()) == 'b' || curr() == '-') { + } else if (curr() == '-') { + read_single_line_comment(); + break; + } else if (normalize(curr()) == 'b') { return read_b_symbol('-'); } else { m_name_val = name("-"); diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index 864959f04..35ed13a09 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -47,6 +47,7 @@ protected: bool check_next(char c); bool check_next_is_digit(); void read_comment(); + void read_single_line_comment(); name mk_name(name const & curr, std::string const & buf, bool only_digits); token read_a_symbol(); token read_b_symbol(char prev); diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index bf16c8f16..128a73191 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -102,8 +102,8 @@ static void tst3() { parse_error(env, ios, "Notation 10 : Int::add"); parse_error(env, ios, "Notation 10 _ : Int::add"); parse(env, ios, "Notation 10 _ ++ _ : Int::add. Eval 10 ++ 20."); - parse(env, ios, "Notation 10 _ -- : Int::neg. Eval 10 --"); - parse(env, ios, "Notation 30 -- _ : Int::neg. Eval -- 10"); + parse(env, ios, "Notation 10 _ -+ : Int::neg. Eval 10 -+"); + parse(env, ios, "Notation 30 -+ _ : Int::neg. Eval -+ 10"); parse_error(env, ios, "10 + 30"); } diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp index 8d0ddc08a..646110bd7 100644 --- a/src/tests/frontends/lean/scanner.cpp +++ b/src/tests/frontends/lean/scanner.cpp @@ -69,8 +69,7 @@ static void check_name(char const * str, name const & expected) { } static void tst1() { - scan("fun(x: Pi A : Type, A -> A), (* (* test *) *) x+1 = 2.0 λ"); - scan_error("(* (* foo *)"); + scan("fun(x: Pi A : Type, A -> A), x+1 = 2.0 λ"); } static void tst2() { @@ -80,11 +79,11 @@ static void tst2() { check("fun (x : Bool), x", {st::Lambda, st::LeftParen, st::Id, st::Colon, st::Id, st::RightParen, st::Comma, st::Id}); check("+++", {st::Id}); check("x+y", {st::Id, st::Id, st::Id}); - check("(* testing *)", {}); + check("-- testing", {}); check(" 2.31 ", {st::DecimalVal}); check(" 333 22", {st::IntVal, st::IntVal}); check("Int -> Int", {st::Id, st::Arrow, st::Id}); - check("Int --> Int", {st::Id, st::Id, st::Id}); + check("Int -+-> Int", {st::Id, st::Id, st::Id}); check("x := 10", {st::Id, st::Assign, st::IntVal}); check("(x+1):Int", {st::LeftParen, st::Id, st::Id, st::IntVal, st::RightParen, st::Colon, st::Id}); check("{x}", {st::LeftCurlyBracket, st::Id, st::RightCurlyBracket}); diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean index 521ff3620..ae75c0d3a 100644 --- a/tests/lean/arith7.lean +++ b/tests/lean/arith7.lean @@ -1,10 +1,9 @@ Import Int. Eval | -2 | -(* - Unfortunately, we can't write |-2|, because |- is considered a single token. - It is not wise to change that since the symbol |- can be used as the notation for - entailment relation in Lean. -*) + +-- Unfortunately, we can't write |-2|, because |- is considered a single token. +-- It is not wise to change that since the symbol |- can be used as the notation for +-- entailment relation in Lean. Eval |3| Definition x : Int := -3 Eval |x + 1| diff --git a/tests/lean/cast1.lean b/tests/lean/cast1.lean index 55b3948ec..0cc99532d 100644 --- a/tests/lean/cast1.lean +++ b/tests/lean/cast1.lean @@ -8,16 +8,12 @@ Theorem V0 (T : Type) (n : Nat) : (vector T (n + 0)) = (vector T n) := Variable f (n : Nat) (v : vector Int n) : Int Variable m : Nat Variable v1 : vector Int (m + 0) -(* - The following application will fail because (vector Int (m + 0)) and (vector Int m) - are not definitionally equal. -*) +-- The following application will fail because (vector Int (m + 0)) and (vector Int m) +-- are not definitionally equal. Check f m v1 -(* - The next one succeeds using the "casting" operator. - We can do it, because (V0 Int m) is a proof that - (vector Int (m + 0)) and (vector Int m) are propositionally equal. - That is, they have the same interpretation in the lean set theoretic - semantics. -*) +-- The next one succeeds using the "casting" operator. +-- We can do it, because (V0 Int m) is a proof that +-- (vector Int (m + 0)) and (vector Int m) are propositionally equal. +-- That is, they have the same interpretation in the lean set theoretic +-- semantics. Check f m (cast (V0 Int m) v1) diff --git a/tests/lean/cast1.lean.expected.out b/tests/lean/cast1.lean.expected.out index 3d8b916fe..7a2e8fd61 100644 --- a/tests/lean/cast1.lean.expected.out +++ b/tests/lean/cast1.lean.expected.out @@ -8,7 +8,7 @@ Assumed: f Assumed: m Assumed: v1 -Error (line: 15, pos: 6) type mismatch at application +Error (line: 13, pos: 7) type mismatch at application f m v1 Function type: Π (n : ℕ), vector ℤ n → ℤ diff --git a/tests/lean/config.lean b/tests/lean/config.lean index 3f5ee410a..a24d59dc4 100644 --- a/tests/lean/config.lean +++ b/tests/lean/config.lean @@ -1,3 +1,3 @@ -(* SetOption default configuration for tests *) +-- SetOption default configuration for tests SetOption pp::colors false SetOption pp::unicode true diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean index a86160fd3..c4556b0a1 100644 --- a/tests/lean/ex2.lean +++ b/tests/lean/ex2.lean @@ -1,5 +1,4 @@ -(* comment *) -(* (* nested comment *) *) +-- comment Show true SetOption lean::pp::notation false Show true && false diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out index 074459e4d..f0f72d9c4 100644 --- a/tests/lean/ex2.lean.expected.out +++ b/tests/lean/ex2.lean.expected.out @@ -6,11 +6,11 @@ and ⊤ ⊥ Set: pp::unicode and true false Assumed: a -Error (line: 9, pos: 0) invalid object declaration, environment already has an object named 'a' +Error (line: 8, pos: 0) invalid object declaration, environment already has an object named 'a' Assumed: b and a b Assumed: A -Error (line: 13, pos: 11) type mismatch at application +Error (line: 12, pos: 11) type mismatch at application and a A Function type: Bool -> Bool -> Bool @@ -19,7 +19,7 @@ Arguments types: A : Type Variable A : Type (lean::pp::notation := false, pp::unicode := false, pp::colors := false) -Error (line: 16, pos: 10) unknown option 'lean::p::notation', type 'Help Options.' for list of available options -Error (line: 17, pos: 29) invalid option value, given option is not an integer +Error (line: 15, pos: 10) unknown option 'lean::p::notation', type 'Help Options.' for list of available options +Error (line: 16, pos: 29) invalid option value, given option is not an integer Set: lean::pp::notation a /\ b diff --git a/tests/lean/implicit1.lean b/tests/lean/implicit1.lean index 956c4cf48..59829cf61 100644 --- a/tests/lean/implicit1.lean +++ b/tests/lean/implicit1.lean @@ -11,12 +11,10 @@ Show forall a b, g a (f a b) > 0 Show fun a, a + 1 Show fun a b, a + b Show fun (a b) (c : Int), a + c + b -(* - The next example shows a limitation of the current elaborator. - The current elaborator resolves overloads before solving the implicit argument constraints. - So, it does not have enough information for deciding which overload to use. -*) +-- The next example shows a limitation of the current elaborator. +-- The current elaborator resolves overloads before solving the implicit argument constraints. +-- So, it does not have enough information for deciding which overload to use. Show (fun a b, a + b) 10 20. Variable x : Int -(* The following one works because the type of x is used to decide which + should be used *) +-- The following one works because the type of x is used to decide which + should be used Show fun a b, a + x + b \ No newline at end of file diff --git a/tests/lean/implicit7.lean b/tests/lean/implicit7.lean index f6220ab39..9e2024f63 100644 --- a/tests/lean/implicit7.lean +++ b/tests/lean/implicit7.lean @@ -1,9 +1,3 @@ -(* - TODO(Leo): - Improve elaborator's performance on this example. - The main problem is that we don't have any indexing technique - for the elaborator. -*) Variable f {A : Type} (a : A) {B : Type} : A -> B -> A Variable g {A B : Type} (a : A) {C : Type} : B -> C -> C Notation 100 _ ; _ ; _ : f diff --git a/tests/lean/interactive/config.lean b/tests/lean/interactive/config.lean index 3f5ee410a..a24d59dc4 100644 --- a/tests/lean/interactive/config.lean +++ b/tests/lean/interactive/config.lean @@ -1,3 +1,3 @@ -(* SetOption default configuration for tests *) +-- SetOption default configuration for tests SetOption pp::colors false SetOption pp::unicode true diff --git a/tests/lean/interactive/t12.lean b/tests/lean/interactive/t12.lean index 482df8029..b3540b3e8 100644 --- a/tests/lean/interactive/t12.lean +++ b/tests/lean/interactive/t12.lean @@ -4,56 +4,36 @@ import("tactic.lua") auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac())) **) -(* -The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it. -The "hint" is a tactic that should be used to fill the "hole". -In the following example, we use the tactic "auto" defined by the Lua code above. - -The (show [expr] by [tactic]) expression is also creating a "hole" and associating a "hint" to it. -The expression [expr] after the shows is fixing the type of the "hole" -*) Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 : A := (by auto), lemma2 : B := (by auto) in (show B /\ A by auto) -Show Environment 1. (* Show proof for the previous theorem *) +Show Environment 1. -- Show proof for the previous theorem -(* -When hints are not provided, the user must fill the (remaining) holes using tactic command sequences. -Each hole must be filled with a tactic command sequence that terminates with the command 'done' and -successfully produces a proof term for filling the hole. Here is the same example without hints -This style is more convenient for interactive proofs -*) Theorem T2 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, - let lemma1 : A := _, (* first hole *) - lemma2 : B := _ (* second hole *) - in _. (* third hole *) - auto. done. (* tactic command sequence for the first hole *) - auto. done. (* tactic command sequence for the second hole *) - auto. done. (* tactic command sequence for the third hole *) + let lemma1 : A := _, + lemma2 : B := _ + in _. + auto. done. + auto. done. + auto. done. -(* -In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics. -*) Theorem T3 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, - let lemma1 : A := _, (* first hole *) - lemma2 : B := _ (* second hole *) - in _. (* third hole *) - conj_hyp. exact. done. (* tactic command sequence for the first hole *) - conj_hyp. exact. done. (* tactic command sequence for the second hole *) - apply Conj. exact. done. (* tactic command sequence for the third hole *) + let lemma1 : A := _, + lemma2 : B := _ + in _. + conj_hyp. exact. done. + conj_hyp. exact. done. + apply Conj. exact. done. -(* -We can also mix the two styles (hints and command sequences) -*) Theorem T4 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, - let lemma1 : A := _, (* first hole *) - lemma2 : B := _ (* second hole *) + let lemma1 : A := _, + lemma2 : B := _ in (show B /\ A by auto). - conj_hyp. exact. done. (* tactic command sequence for the first hole *) - conj_hyp. exact. done. (* tactic command sequence for the second hole *) + conj_hyp. exact. done. + conj_hyp. exact. done. diff --git a/tests/lean/let2.lean b/tests/lean/let2.lean index bcfae2441..2342e9ae8 100644 --- a/tests/lean/let2.lean +++ b/tests/lean/let2.lean @@ -1,5 +1,4 @@ - -(* Annotating lemmas *) +-- Annotating lemmas Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r := Discharge (λ H_pq_qr, Discharge (λ H_p, diff --git a/tests/lean/push.lean b/tests/lean/push.lean index 0af009078..6e0cf781b 100644 --- a/tests/lean/push.lean +++ b/tests/lean/push.lean @@ -8,7 +8,7 @@ Push Eval f a Pop -Eval f a (* should produce an error *) +Eval f a -- should produce an error Show Environment 1 @@ -17,6 +17,6 @@ Push Check 10 ++ 20 Pop -Check 10 ++ 20 (* should produce an error *) +Check 10 ++ 20 -- should produce an error -Pop (* should produce an error *) \ No newline at end of file +Pop -- should produce an error \ No newline at end of file diff --git a/tests/lean/single.lean b/tests/lean/single.lean index b2821c266..6a9513fa9 100644 --- a/tests/lean/single.lean +++ b/tests/lean/single.lean @@ -3,5 +3,5 @@ Variables a b c : Int. Show a + b + c. Check a + b. Exit. -(* the following line should be executed *) +-- the following line should be executed Check a + true. diff --git a/tests/lean/slow/config.lean b/tests/lean/slow/config.lean index 3f5ee410a..a24d59dc4 100644 --- a/tests/lean/slow/config.lean +++ b/tests/lean/slow/config.lean @@ -1,3 +1,3 @@ -(* SetOption default configuration for tests *) +-- SetOption default configuration for tests SetOption pp::colors false SetOption pp::unicode true diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean index 0c52f1a2b..42bc9900f 100644 --- a/tests/lean/tactic2.lean +++ b/tests/lean/tactic2.lean @@ -8,9 +8,9 @@ Theorem T1 : p => q => p /\ q := H2 : q := _ in Conj H1 H2 )). - exact (* solve first metavar *) + exact -- solve first metavar done - exact (* solve second metavar *) + exact -- solve second metavar done (** @@ -27,12 +27,12 @@ Theorem T3 : p => p /\ q => r => q /\ r /\ p := _. (** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **) done -(* Display proof term generated by previous tac *) +-- Display proof term generated by previous tac Show Environment 1 Theorem T4 : p => p /\ q => r => q /\ r /\ p := _. Repeat (OrElse (apply Discharge) (apply Conj) conj_hyp exact) done -(* Display proof term generated by previous tac *) +-- Display proof term generated by previous tac -- Show Environment 1 \ No newline at end of file diff --git a/tests/lean/tactic3.lean b/tests/lean/tactic3.lean index 115dcba5a..e60202029 100644 --- a/tests/lean/tactic3.lean +++ b/tests/lean/tactic3.lean @@ -5,5 +5,5 @@ Theorem T1 : p => p /\ q => r => q /\ r /\ p := _. (** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **) done -(* Display proof term generated by previous tactic *) +-- Display proof term generated by previous tactic Show Environment 1 \ No newline at end of file diff --git a/tests/lean/tst1.lean b/tests/lean/tst1.lean index b28239eff..27cecadee 100644 --- a/tests/lean/tst1.lean +++ b/tests/lean/tst1.lean @@ -1,4 +1,4 @@ -(* Define a "fake" type to simulate the natural numbers. This is just a test. *) +-- Define a "fake" type to simulate the natural numbers. This is just a test. Variable N : Type Variable lt : N -> N -> Bool Variable zero : N diff --git a/tests/lean/tst10.lean b/tests/lean/tst10.lean index 84ac75456..a6813c71d 100644 --- a/tests/lean/tst10.lean +++ b/tests/lean/tst10.lean @@ -1,24 +1,24 @@ Variable a : Bool Variable b : Bool -(* Conjunctions *) +-- Conjunctions Show a && b Show a && b && a Show a /\ b Show a ∧ b Show (and a b) Show and a b -(* Disjunctions *) +-- Disjunctions Show a || b Show a \/ b Show a ∨ b Show (or a b) Show or a (or a b) -(* Simple Formulas *) +-- Simple Formulas Show a => b => a Check a => b Eval a => a Eval true => a -(* Simple proof *) +-- Simple proof Axiom H1 : a Axiom H2 : a => b Check @MP diff --git a/tests/lean/tst6.lean b/tests/lean/tst6.lean index ad4e17799..74c05a378 100644 --- a/tests/lean/tst6.lean +++ b/tests/lean/tst6.lean @@ -4,11 +4,11 @@ Variable h : N -> N -> N Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2 -(* Display the theorem showing implicit arguments *) +-- Display the theorem showing implicit arguments SetOption lean::pp::implicit true Show Environment 2 -(* Display the theorem hiding implicit arguments *) +-- Display the theorem hiding implicit arguments SetOption lean::pp::implicit false Show Environment 2 @@ -19,11 +19,11 @@ Theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h (fun H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) -(* Show proof of the last theorem with all implicit arguments *) +-- Show proof of the last theorem with all implicit arguments SetOption lean::pp::implicit true Show Environment 1 -(* Using placeholders to hide the type of H1 *) +-- Using placeholders to hide the type of H1 Theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := DisjCases H (fun H1 : _, @@ -34,7 +34,7 @@ Theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h SetOption lean::pp::implicit true Show Environment 1 -(* Same example but the first conjuct has unnecessary stuff *) +-- Same example but the first conjuct has unnecessary stuff Theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := DisjCases H (fun H1 : _, diff --git a/tests/lean/tst7.lean b/tests/lean/tst7.lean index b72d2bfab..724c8557b 100644 --- a/tests/lean/tst7.lean +++ b/tests/lean/tst7.lean @@ -1,6 +1,6 @@ Variable f : Pi (A : Type), A -> Bool Show fun (A B : Type) (a : _), f B a -(* The following one should produce an error *) +-- The following one should produce an error Show fun (A : Type) (a : _) (B : Type), f B a Variable myeq : Pi A : (Type U), A -> A -> Bool diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out index 1947b4e7f..26065b95d 100644 --- a/tests/lean/tst7.lean.expected.out +++ b/tests/lean/tst7.lean.expected.out @@ -4,7 +4,7 @@ λ (A B : Type) (a : B), f B a Failed to solve A : Type, a : ?M::0, B : Type ⊢ ?M::0[lift:0:2] ≺ B - (line: 4: pos: 40) Type of argument 2 must be convertible to the expected type in the application of + (line: 4: pos: 41) Type of argument 2 must be convertible to the expected type in the application of f with arguments: B diff --git a/tests/lua/coercion_bug1.lua b/tests/lua/coercion_bug1.lua index 09c35bc1c..5c19e8125 100644 --- a/tests/lua/coercion_bug1.lua +++ b/tests/lua/coercion_bug1.lua @@ -4,13 +4,13 @@ parse_lean_cmds([[ Variable f : Int -> Int -> Int Notation 20 _ +++ _ : f Show f 10 20 - Notation 20 _ --- _ : f + Notation 20 _ -+- _ : f Show f 10 20 ]], env) local F = parse_lean('f 10 20', env) print(lean_formatter(env)(F)) -assert(tostring(lean_formatter(env)(F)) == "10 --- 20") +assert(tostring(lean_formatter(env)(F)) == "10 -+- 20") local child = env:mk_child() @@ -18,6 +18,6 @@ parse_lean_cmds([[ Show f 10 20 ]], child) -assert(tostring(lean_formatter(env)(F)) == "10 --- 20") +assert(tostring(lean_formatter(env)(F)) == "10 -+- 20") print(lean_formatter(child)(F)) -assert(tostring(lean_formatter(child)(F)) == "10 --- 20") +assert(tostring(lean_formatter(child)(F)) == "10 -+- 20") diff --git a/tests/lua/front.lua b/tests/lua/front.lua index 9b881dc9c..fc7627730 100644 --- a/tests/lua/front.lua +++ b/tests/lua/front.lua @@ -27,7 +27,7 @@ parse_lean_cmds([[ Variable f : Int -> Int -> Int Variables a b : Int Show f a b -Notation 100 _ -- _ : f +Notation 100 _ -+ _ : f ]], env2) local f, a, b = Consts("f, a, b") @@ -35,7 +35,7 @@ assert(tostring(f(a, b)) == "f a b") set_formatter(lean_formatter(env)) assert(tostring(f(a, b)) == "a ++ b") set_formatter(lean_formatter(env2)) -assert(tostring(f(a, b)) == "a -- b") +assert(tostring(f(a, b)) == "a -+ b") local fmt = lean_formatter(env) -- We can parse commands with respect to environment env2,