From dd72269b139cb83dda061b5f9b92b5b8ff28edf3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Dec 2013 21:18:45 -0800 Subject: [PATCH] feat(frontends/lean): rename command Set to SetOption It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean Signed-off-by: Leonardo de Moura --- examples/lean/ex1.lean | 4 ++-- examples/lean/ex2.lean | 2 +- examples/lean/set.lean | 14 +++++++------- src/frontends/lean/parser.cpp | 6 +++--- src/tests/frontends/lean/parser.cpp | 10 +++++----- tests/lean/abst.lean | 2 +- tests/lean/arith1.lean | 4 ++-- tests/lean/arith2.lean | 2 +- tests/lean/arith3.lean | 2 +- tests/lean/arith6.lean | 4 ++-- tests/lean/arith7.lean | 2 +- tests/lean/bad2.lean | 4 ++-- tests/lean/cast2.lean | 2 +- tests/lean/coercion2.lean | 10 +++++----- tests/lean/config.lean | 6 +++--- tests/lean/elab4.lean | 2 +- tests/lean/elab5.lean | 2 +- tests/lean/elab7.lean | 2 +- tests/lean/eq1.lean | 2 +- tests/lean/eq2.lean | 2 +- tests/lean/eq3.lean | 2 +- tests/lean/ex2.lean | 10 +++++----- tests/lean/ex2.lean.expected.out | 4 ++-- tests/lean/ex3.lean | 2 +- tests/lean/implicit1.lean | 2 +- tests/lean/implicit2.lean | 2 +- tests/lean/implicit3.lean | 4 ++-- tests/lean/implicit6.lean | 4 ++-- tests/lean/implicit7.lean | 4 ++-- tests/lean/interactive/config.lean | 6 +++--- tests/lean/interactive/t8.lean | 2 +- tests/lean/let1.lean | 2 +- tests/lean/let3.lean | 4 ++-- tests/lean/let4.lean | 2 +- tests/lean/lua6.lean | 2 +- tests/lean/overload1.lean | 2 +- tests/lean/overload2.lean | 4 ++-- tests/lean/slow/config.lean | 6 +++--- tests/lean/slow/deep.lean | 4 ++-- tests/lean/subst.lean | 6 +++--- tests/lean/tactic7.lean | 2 +- tests/lean/tst2.lean | 4 ++-- tests/lean/tst3.lean | 24 ++++++++++++------------ tests/lean/tst4.lean | 2 +- tests/lean/tst5.lean | 2 +- tests/lean/tst6.lean | 12 ++++++------ tests/lean/unicode.lean | 8 ++++---- tests/lua/front.lua | 4 ++-- tests/lua/parser2.lua | 6 +++--- 49 files changed, 111 insertions(+), 111 deletions(-) diff --git a/examples/lean/ex1.lean b/examples/lean/ex1.lean index 39d11bffa..244f44d9e 100644 --- a/examples/lean/ex1.lean +++ b/examples/lean/ex1.lean @@ -30,6 +30,6 @@ Theorem T2 : (h a (h a b)) = (h a (h c e)) := Show Environment 2 (* Show implicit arguments *) -Set lean::pp::implicit true -Set pp::width 150 +SetOption lean::pp::implicit true +SetOption pp::width 150 Show Environment 2 diff --git a/examples/lean/ex2.lean b/examples/lean/ex2.lean index 8aa95530e..7bac88cbc 100644 --- a/examples/lean/ex2.lean +++ b/examples/lean/ex2.lean @@ -5,7 +5,7 @@ Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r := P_q := MP P_pq H_p in MP P_qr P_q)) -Set pp::implicit true +SetOption pp::implicit true Show Environment 1 Theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c := diff --git a/examples/lean/set.lean b/examples/lean/set.lean index e3da52052..437bd32a2 100644 --- a/examples/lean/set.lean +++ b/examples/lean/set.lean @@ -1,15 +1,15 @@ -Definition set (A : Type) : Type := A -> Bool +Definition Set (A : Type) : Type := A -> Bool -Definition element {A : Type} (x : A) (s : set A) := s x +Definition element {A : Type} (x : A) (s : Set A) := s x Infix 60 ∈ : element -Definition subset {A : Type} (s1 : set A) (s2 : set A) := ∀ x, x ∈ s1 ⇒ x ∈ s2 +Definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 ⇒ x ∈ s2 Infix 50 ⊆ : subset -Theorem SubsetProp {A : Type} {s1 s2 : set A} {x : A} (H1 : s1 ⊆ s2) (H2 : x ∈ s1) : x ∈ s2 := +Theorem SubsetProp {A : Type} {s1 s2 : Set A} {x : A} (H1 : s1 ⊆ s2) (H2 : x ∈ s1) : x ∈ s2 := MP (ForallElim H1 x) H2 -Theorem SubsetTrans {A : Type} {s1 s2 s3 : set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3 := +Theorem SubsetTrans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3 := ForallIntro (λ x, Discharge (λ Hin : x ∈ s1, let L1 : x ∈ s2 := SubsetProp H1 Hin, @@ -23,8 +23,8 @@ Theorem SubsetTrans2 {A : Type} : transitive (subset::explicit A) := Discharge (λ H1, (Discharge (λ H2, SubsetTrans H1 H2)))))). -Theorem SubsetRefl {A : Type} (s : set A) : s ⊆ s := +Theorem SubsetRefl {A : Type} (s : Set A) : s ⊆ s := ForallIntro (λ x, Discharge (λ H : x ∈ s, H)) -Definition union {A : Type} (s1 : set A) (s2 : set A) := λ x, x ∈ s1 ∨ x ∈ s2 +Definition union {A : Type} (s1 : Set A) (s2 : Set A) := λ x, x ∈ s1 ∨ x ∈ s2 Infix 55 ∪ : union diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index a9c960d21..e97b452e3 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -90,7 +90,7 @@ static name g_infixl_kwd("Infixl"); static name g_infixr_kwd("Infixr"); static name g_notation_kwd("Notation"); static name g_echo_kwd("Echo"); -static name g_set_kwd("Set"); +static name g_set_kwd("SetOption"); static name g_options_kwd("Options"); static name g_env_kwd("Environment"); static name g_import_kwd("Import"); @@ -1958,7 +1958,7 @@ class parser::imp { regular(m_io_state) << msg << endl; } - /** Parse 'Set' [id] [value] */ + /** Parse 'SetOption' [id] [value] */ void parse_set() { next(); auto id_pos = pos(); @@ -2065,7 +2065,7 @@ class parser::imp { << " Push create a scope (it is just an alias for the command Scope)" << endl << " Pop discard the current scope" << endl << " Scope create a scope" << endl - << " Set [id] [value] set option [id] with value [value]" << endl + << " SetOption [id] [value] set option [id] with value [value]" << endl << " Show [expr] pretty print the given expression" << endl << " Show Options show current the set of assigned options" << endl << " Show Environment show objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index d11d39c5f..1756b793f 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -93,11 +93,11 @@ static void tst3() { parse_error(env, ios, "Check U"); parse(env, ios, "Variable h : Real -> Real -> Real. Notation 10 [ _ ; _ ] : h. Check [ 10.3 ; 20.1 ]."); parse_error(env, ios, "Variable h : Real -> Real -> Real. Notation 10 [ _ ; _ ] : h. Check [ 10.3 | 20.1 ]."); - parse_error(env, ios, "Set pp::indent true"); - parse(env, ios, "Set pp::indent 10"); - parse_error(env, ios, "Set pp::colors foo"); - parse_error(env, ios, "Set pp::colors \"foo\""); - parse(env, ios, "Set pp::colors true"); + parse_error(env, ios, "SetOption pp::indent true"); + parse(env, ios, "SetOption pp::indent 10"); + parse_error(env, ios, "SetOption pp::colors foo"); + parse_error(env, ios, "SetOption pp::colors \"foo\""); + parse(env, ios, "SetOption pp::colors true"); 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."); diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean index 960f40e5e..274954434 100644 --- a/tests/lean/abst.lean +++ b/tests/lean/abst.lean @@ -1,5 +1,5 @@ Axiom PlusComm(a b : Int) : a + b == b + a. Variable a : Int. Check (Abst (fun x : Int, (PlusComm a x))). -Set pp::implicit true. +SetOption pp::implicit true. Check (Abst (fun x : Int, (PlusComm a x))). diff --git a/tests/lean/arith1.lean b/tests/lean/arith1.lean index c6d69929c..800fd8db4 100644 --- a/tests/lean/arith1.lean +++ b/tests/lean/arith1.lean @@ -9,9 +9,9 @@ Variable n : Nat Variable m : Nat Show n + m Show n + x + m -Set lean::pp::coercion true +SetOption lean::pp::coercion true Show n + x + m + 10 Show x + n + m + 10 Show n + m + 10 + x -Set lean::pp::notation false +SetOption lean::pp::notation false Show n + m + 10 + x diff --git a/tests/lean/arith2.lean b/tests/lean/arith2.lean index dc7bc11b8..1f38da611 100644 --- a/tests/lean/arith2.lean +++ b/tests/lean/arith2.lean @@ -5,7 +5,7 @@ Variable x : Real Variable i : Int Variable n : Nat Show x + i + 1 + n -Set lean::pp::coercion true +SetOption lean::pp::coercion true Show x + i + 1 + n Show x * i + x Show x - i + x - x >= 0 diff --git a/tests/lean/arith3.lean b/tests/lean/arith3.lean index 25b4427a3..d805e61ab 100644 --- a/tests/lean/arith3.lean +++ b/tests/lean/arith3.lean @@ -3,7 +3,7 @@ Eval 8 div 4 Eval 7 div 3 Eval 7 mod 3 Show -8 mod 3 -Set lean::pp::notation false +SetOption lean::pp::notation false Show -8 mod 3 Eval -8 mod 3 Eval (-8 div 3)*3 + (-8 mod 3) \ No newline at end of file diff --git a/tests/lean/arith6.lean b/tests/lean/arith6.lean index 42798cc1d..2cb769c01 100644 --- a/tests/lean/arith6.lean +++ b/tests/lean/arith6.lean @@ -1,4 +1,4 @@ -Set pp::unicode false +SetOption pp::unicode false Show 3 | 6 Eval 3 | 6 Eval 3 | 7 @@ -8,5 +8,5 @@ Variable x : Int Eval x | 3 Eval 3 | x Eval 6 | 3 -Set pp::notation false +SetOption pp::notation false Show 3 | x \ No newline at end of file diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean index e4485dac3..b004e422f 100644 --- a/tests/lean/arith7.lean +++ b/tests/lean/arith7.lean @@ -11,6 +11,6 @@ Eval |x + 1| > 0 Variable y : Int Eval |x + y| Show |x + y| > x -Set pp::notation false +SetOption pp::notation false Show |x + y| > x Show |x + y| + |y + x| > x \ No newline at end of file diff --git a/tests/lean/bad2.lean b/tests/lean/bad2.lean index f0a3902b0..9fa112edc 100644 --- a/tests/lean/bad2.lean +++ b/tests/lean/bad2.lean @@ -7,6 +7,6 @@ Definition n3 : list Int := cons 10 nil Definition n4 : list Int := nil Definition n5 : _ := cons 10 nil -Set pp::coercion true -Set pp::implicit true +SetOption pp::coercion true +SetOption pp::implicit true Show Environment 1. \ No newline at end of file diff --git a/tests/lean/cast2.lean b/tests/lean/cast2.lean index 32cc69b36..09f7cc769 100644 --- a/tests/lean/cast2.lean +++ b/tests/lean/cast2.lean @@ -6,6 +6,6 @@ Axiom H : (A -> B) = (A' -> B') Variable a : A Check DomInj H Theorem BeqB' : B = B' := RanInj H a -Set pp::implicit true +SetOption pp::implicit true Show DomInj H Show RanInj H a diff --git a/tests/lean/coercion2.lean b/tests/lean/coercion2.lean index 12253dad7..819cd2117 100644 --- a/tests/lean/coercion2.lean +++ b/tests/lean/coercion2.lean @@ -8,25 +8,25 @@ Show g a a Variable b : R Show g a b Show g b a -Set lean::pp::coercion true +SetOption lean::pp::coercion true Show g a a Show g a b Show g b a -Set lean::pp::coercion false +SetOption lean::pp::coercion false Variable S : Type Variable s : S Variable r : S Variable h : S -> S -> S Infixl 10 ++ : g Infixl 10 ++ : h -Set lean::pp::notation false +SetOption lean::pp::notation false Show a ++ b ++ a Show r ++ s ++ r Check a ++ b ++ a Check r ++ s ++ r -Set lean::pp::coercion true +SetOption lean::pp::coercion true Show a ++ b ++ a Show r ++ s ++ r -Set lean::pp::notation true +SetOption lean::pp::notation true Show a ++ b ++ a Show r ++ s ++ r diff --git a/tests/lean/config.lean b/tests/lean/config.lean index 905e75340..3f5ee410a 100644 --- a/tests/lean/config.lean +++ b/tests/lean/config.lean @@ -1,3 +1,3 @@ -(* Set default configuration for tests *) -Set pp::colors false -Set pp::unicode true +(* SetOption default configuration for tests *) +SetOption pp::colors false +SetOption pp::unicode true diff --git a/tests/lean/elab4.lean b/tests/lean/elab4.lean index 026610862..eb5d02b05 100644 --- a/tests/lean/elab4.lean +++ b/tests/lean/elab4.lean @@ -8,5 +8,5 @@ Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 := fun A1 A2 B1 B2 H a, R H a -Set pp::implicit true +SetOption pp::implicit true Show Environment 7. diff --git a/tests/lean/elab5.lean b/tests/lean/elab5.lean index 619148a65..aefa79b6c 100644 --- a/tests/lean/elab5.lean +++ b/tests/lean/elab5.lean @@ -8,5 +8,5 @@ Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) Theorem R2 : Pi (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B2) := fun A1 A2 B1 B2 H a, R H a -Set pp::implicit true +SetOption pp::implicit true Show Environment 7. diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean index 8ccb058b8..fe2f8f070 100644 --- a/tests/lean/elab7.lean +++ b/tests/lean/elab7.lean @@ -19,5 +19,5 @@ Theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := Abst (fun a, (Abst (fun b Theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := Abst (fun a, (Abst (fun b, H a b))) Theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := Abst (fun a, (Abst (fun b, H a b))) Show Environment 4 -Set pp::implicit true +SetOption pp::implicit true Show Environment 4 \ No newline at end of file diff --git a/tests/lean/eq1.lean b/tests/lean/eq1.lean index 8af2b670b..ef8c66b17 100644 --- a/tests/lean/eq1.lean +++ b/tests/lean/eq1.lean @@ -1,5 +1,5 @@ Variable i : Int Check i = 0 -Set pp::coercion true +SetOption pp::coercion true Check i = 0 diff --git a/tests/lean/eq2.lean b/tests/lean/eq2.lean index 9c5ffeef4..44f17718d 100644 --- a/tests/lean/eq2.lean +++ b/tests/lean/eq2.lean @@ -3,5 +3,5 @@ Variable nil {A : Type} : List A Variable cons {A : Type} (head : A) (tail : List A) : List A Variable l : List Int. Check l = nil. -Set pp::implicit true +SetOption pp::implicit true Check l = nil. diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean index 3d840ea79..a426ea237 100644 --- a/tests/lean/eq3.lean +++ b/tests/lean/eq3.lean @@ -8,5 +8,5 @@ Variable v3 : Vector (0 + n) Axiom H1 : v1 == v2 Axiom H2 : v2 == v3 Check TransExt H1 H2 -Set pp::implicit true +SetOption pp::implicit true Check TransExt H1 H2 diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean index aba386fa7..a86160fd3 100644 --- a/tests/lean/ex2.lean +++ b/tests/lean/ex2.lean @@ -1,9 +1,9 @@ (* comment *) (* (* nested comment *) *) Show true -Set lean::pp::notation false +SetOption lean::pp::notation false Show true && false -Set pp::unicode false +SetOption pp::unicode false Show true && false Variable a : Bool Variable a : Bool @@ -13,7 +13,7 @@ Variable A : Type Check a && A Show Environment 1 Show Options -Set lean::p::notation true -Set lean::pp::notation 10 -Set lean::pp::notation true +SetOption lean::p::notation true +SetOption lean::pp::notation 10 +SetOption lean::pp::notation true Show a && b diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out index dd6fbed28..074459e4d 100644 --- a/tests/lean/ex2.lean.expected.out +++ b/tests/lean/ex2.lean.expected.out @@ -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: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options -Error (line: 17, pos: 23) invalid option value, given option is not an integer +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 Set: lean::pp::notation a /\ b diff --git a/tests/lean/ex3.lean b/tests/lean/ex3.lean index 9154da3c8..e5dda70db 100644 --- a/tests/lean/ex3.lean +++ b/tests/lean/ex3.lean @@ -5,5 +5,5 @@ Variable a : T Check myeq _ true a Variable myeq2 {A:Type} (a b : A) : Bool Infix 50 === : myeq2 -Set lean::pp::implicit true +SetOption lean::pp::implicit true Check true === a \ No newline at end of file diff --git a/tests/lean/implicit1.lean b/tests/lean/implicit1.lean index ed7049971..575f9145a 100644 --- a/tests/lean/implicit1.lean +++ b/tests/lean/implicit1.lean @@ -4,7 +4,7 @@ Show forall a b, f a b > 0 Variable g : Int -> Real -> Int Show forall a b, g a b > 0 Show forall a b, g a (f a b) > 0 -Set pp::coercion true +SetOption pp::coercion true Show forall a b, g a (f a b) > 0 Show fun a, a + 1 Show fun a b, a + b diff --git a/tests/lean/implicit2.lean b/tests/lean/implicit2.lean index 343b03582..da78a04c7 100644 --- a/tests/lean/implicit2.lean +++ b/tests/lean/implicit2.lean @@ -7,6 +7,6 @@ Check g 10 20 true Check let r : Real -> Real -> Real := g 10 20 in r Check g 10 -Set pp::implicit true +SetOption pp::implicit true Check let r : Real -> Real -> Real := g 10 20 in r diff --git a/tests/lean/implicit3.lean b/tests/lean/implicit3.lean index 5d527facc..a5b6722a5 100644 --- a/tests/lean/implicit3.lean +++ b/tests/lean/implicit3.lean @@ -3,7 +3,7 @@ Variable f : Int -> Int -> Int Variable g : Int -> Int -> Int -> Int Notation 10 _ ++ _ : f Notation 10 _ ++ _ : g -Set pp::implicit true -Set pp::notation false +SetOption pp::implicit true +SetOption pp::notation false Show (10 ++ 20) Show (10 ++ 20) 10 diff --git a/tests/lean/implicit6.lean b/tests/lean/implicit6.lean index 871aa7605..683e3c524 100644 --- a/tests/lean/implicit6.lean +++ b/tests/lean/implicit6.lean @@ -3,8 +3,8 @@ Infixl 65 + : f Show true + false Show 10 + 20 Show 10 + (- 20) -Set pp::notation false -Set pp::coercion true +SetOption pp::notation false +SetOption pp::coercion true Show true + false Show 10 + 20 Show 10 + (- 20) diff --git a/tests/lean/implicit7.lean b/tests/lean/implicit7.lean index ebefa0930..f6220ab39 100644 --- a/tests/lean/implicit7.lean +++ b/tests/lean/implicit7.lean @@ -10,9 +10,9 @@ Notation 100 _ ; _ ; _ : f Notation 100 _ ; _ ; _ : g Check 10 ; true ; false Check 10 ; 10 ; true -Set pp::notation false +SetOption pp::notation false Check 10 ; true ; false Check 10 ; 10 ; true -Set pp::implicit true +SetOption pp::implicit true Check 10 ; true ; false Check 10 ; 10 ; true diff --git a/tests/lean/interactive/config.lean b/tests/lean/interactive/config.lean index 905e75340..3f5ee410a 100644 --- a/tests/lean/interactive/config.lean +++ b/tests/lean/interactive/config.lean @@ -1,3 +1,3 @@ -(* Set default configuration for tests *) -Set pp::colors false -Set pp::unicode true +(* SetOption default configuration for tests *) +SetOption pp::colors false +SetOption pp::unicode true diff --git a/tests/lean/interactive/t8.lean b/tests/lean/interactive/t8.lean index 76fd33d14..00609943b 100644 --- a/tests/lean/interactive/t8.lean +++ b/tests/lean/interactive/t8.lean @@ -1,4 +1,4 @@ -Set tactic::proof_state::goal_names true. +SetOption tactic::proof_state::goal_names true. Theorem T (a : Bool) : a => a /\ a. apply imp_tac. apply Conj. diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean index f40d530c3..fb565b3d5 100644 --- a/tests/lean/let1.lean +++ b/tests/lean/let1.lean @@ -5,7 +5,7 @@ Check let a : Nat := 10 in a + 1 Eval let a : Nat := 20 in a + 10 Eval let a := 20 in a + 10 Check let a : Int := 20 in a + 10 -Set pp::coercion true +SetOption pp::coercion true Show let a : Int := 20 in a + 10 diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean index 1da0fd807..fcc1f8771 100644 --- a/tests/lean/let3.lean +++ b/tests/lean/let3.lean @@ -1,8 +1,8 @@ Variable magic : Pi (H : Bool), H -Set pp::notation false -Set pp::coercion true +SetOption pp::notation false +SetOption pp::coercion true Show let a : Int := 1, H : a > 0 := magic (a > 0) in H \ No newline at end of file diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean index 90c2f77c9..68afeb5e3 100644 --- a/tests/lean/let4.lean +++ b/tests/lean/let4.lean @@ -40,7 +40,7 @@ let a := 10, v2 : vector Int a := v1 in v2 -Set pp::coercion true +SetOption pp::coercion true Show let a := 10, diff --git a/tests/lean/lua6.lean b/tests/lean/lua6.lean index b061065c1..7002dd78c 100644 --- a/tests/lean/lua6.lean +++ b/tests/lean/lua6.lean @@ -1,5 +1,5 @@ Variable x : Int -Set pp::notation false +SetOption pp::notation false (** print(get_options()) **) diff --git a/tests/lean/overload1.lean b/tests/lean/overload1.lean index b7b999bec..993d22558 100644 --- a/tests/lean/overload1.lean +++ b/tests/lean/overload1.lean @@ -4,7 +4,7 @@ Variable g : N -> N -> N Infixl 10 ++ : f Infixl 10 ++ : g Show true ++ false ++ true -Set lean::pp::notation false +SetOption lean::pp::notation false Show true ++ false ++ true Variable a : N Variable b : N diff --git a/tests/lean/overload2.lean b/tests/lean/overload2.lean index 6c238c5d7..2798b0990 100644 --- a/tests/lean/overload2.lean +++ b/tests/lean/overload2.lean @@ -8,8 +8,8 @@ Coercion t2r Variable f : T -> R -> T Variable a : T Variable b : R -Set lean::pp::coercion true -Set lean::pp::notation false +SetOption lean::pp::coercion true +SetOption lean::pp::notation false Show f a b Show f b a Variable g : R -> T -> R diff --git a/tests/lean/slow/config.lean b/tests/lean/slow/config.lean index 905e75340..3f5ee410a 100644 --- a/tests/lean/slow/config.lean +++ b/tests/lean/slow/config.lean @@ -1,3 +1,3 @@ -(* Set default configuration for tests *) -Set pp::colors false -Set pp::unicode true +(* SetOption default configuration for tests *) +SetOption pp::colors false +SetOption pp::unicode true diff --git a/tests/lean/slow/deep.lean b/tests/lean/slow/deep.lean index 1ca9413ae..7a43d2f69 100644 --- a/tests/lean/slow/deep.lean +++ b/tests/lean/slow/deep.lean @@ -2,6 +2,6 @@ Definition f1 (f : Int -> Int) (x : Int) : Int := f (f (f (f x))) Definition f2 (f : Int -> Int) (x : Int) : Int := f1 (f1 (f1 (f1 f))) x Definition f3 (f : Int -> Int) (x : Int) : Int := f1 (f2 (f2 f)) x Variable f : Int -> Int. -Set pp::width 80. -Set lean::pp::max_depth 2000. +SetOption pp::width 80. +SetOption lean::pp::max_depth 2000. Eval f3 f 0. \ No newline at end of file diff --git a/tests/lean/subst.lean b/tests/lean/subst.lean index afbac2cd3..dc7fa1e24 100644 --- a/tests/lean/subst.lean +++ b/tests/lean/subst.lean @@ -3,7 +3,7 @@ Variable n : Nat Axiom H1 : a + a + a = 10 Axiom H2 : a = n Theorem T : a + n + a = 10 := Subst H1 H2 -Set pp::coercion true -Set pp::notation false -Set pp::implicit true +SetOption pp::coercion true +SetOption pp::notation false +SetOption pp::implicit true Show Environment 1. diff --git a/tests/lean/tactic7.lean b/tests/lean/tactic7.lean index cfb58d367..6bcfe2228 100644 --- a/tests/lean/tactic7.lean +++ b/tests/lean/tactic7.lean @@ -23,7 +23,7 @@ Theorem VectorPlus0 (A : Type U) (n : Nat) : (Vector A (n + 0)) === (Vector A n) EqSubst (fun x : Nat, (Vector A x) === (Vector A n)) (EqRefl (Vector A n)) (EqSymm (Plus0 n)) -Set pp::implicit true +SetOption pp::implicit true (* Check fun (A : Type) (n : Nat), VectorPlus0 A n *) Axiom AppendNil {A : Type} {n : Nat} (v : Vector A n) : (EqCast (VectorPlus0 A n) (append v empty)) === v diff --git a/tests/lean/tst2.lean b/tests/lean/tst2.lean index 595725f49..716770211 100644 --- a/tests/lean/tst2.lean +++ b/tests/lean/tst2.lean @@ -2,10 +2,10 @@ Show Options Variable a : Bool Variable b : Bool Show a/\b -Set lean::pp::notation false +SetOption lean::pp::notation false Show Options Show a/\b Show Environment 2 -Set lean::pp::notation true +SetOption lean::pp::notation true Show Options Show a/\b diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean index d370e19cf..b0e69e680 100644 --- a/tests/lean/tst3.lean +++ b/tests/lean/tst3.lean @@ -1,10 +1,10 @@ -Set lean::parser::verbose false. +SetOption lean::parser::verbose false. Notation 10 if _ then _ : implies. Show Environment 1. Show if true then false. Variable a : Bool. Show if true then if a then false. -Set lean::pp::notation false. +SetOption lean::pp::notation false. Show if true then if a then false. Variable A : Type. Variable f : A -> A -> A -> Bool. @@ -14,29 +14,29 @@ Variable c : A. Variable d : A. Variable e : A. Show c |- d ; e. -Set lean::pp::notation true. +SetOption lean::pp::notation true. Show c |- d ; e. Variable fact : A -> A. Notation 20 _ ! : fact. Show c! !. -Set lean::pp::notation false. +SetOption lean::pp::notation false. Show c! !. -Set lean::pp::notation true. +SetOption lean::pp::notation true. Variable g : A -> A -> A. Notation 30 [ _ ; _ ] : g Show [c;d]. Show [c ; [d;e] ]. -Set lean::pp::notation false. +SetOption lean::pp::notation false. Show [c ; [d;e] ]. -Set lean::pp::notation true. +SetOption lean::pp::notation true. Variable h : A -> A -> A. Notation 40 _ << _ end : h. Show Environment 1. Show d << e end. Show [c ; d << e end ]. -Set lean::pp::notation false. +SetOption lean::pp::notation false. Show [c ; d << e end ]. -Set lean::pp::notation true. +SetOption lean::pp::notation true. Variable r : A -> A -> A. Infixl 30 ++ : r. Variable s : A -> A -> A. @@ -46,13 +46,13 @@ Variable p1 : Bool. Variable p2 : Bool. Variable p3 : Bool. Show p1 || p2 && p3. -Set lean::pp::notation false. +SetOption lean::pp::notation false. Show c ** d ++ e ** c. Show p1 || p2 && p3. -Set lean::pp::notation true. +SetOption lean::pp::notation true. Show c = d || d = c. Show not p1 || p2. Show p1 && p3 || p2 && p3. -Set lean::pp::notation false. +SetOption lean::pp::notation false. Show not p1 || p2. Show p1 && p3 || p2 && p3. diff --git a/tests/lean/tst4.lean b/tests/lean/tst4.lean index aa5236d00..7da3817bb 100644 --- a/tests/lean/tst4.lean +++ b/tests/lean/tst4.lean @@ -2,7 +2,7 @@ Variable f {A : Type} (a b : A) : A Variable N : Type Variable n1 : N Variable n2 : N -Set lean::pp::implicit true +SetOption lean::pp::implicit true Show f n1 n2 Show f (fun x : N -> N, x) (fun y : _, y) Variable EqNice {A : Type} (lhs rhs : A) : Bool diff --git a/tests/lean/tst5.lean b/tests/lean/tst5.lean index bc57f3169..75befcf6d 100644 --- a/tests/lean/tst5.lean +++ b/tests/lean/tst5.lean @@ -3,7 +3,7 @@ Variable a : N Variable b : N Show a = b Check a = b -Set lean::pp::implicit true +SetOption lean::pp::implicit true Show a = b Show (Type 1) = (Type 1) Show true = false diff --git a/tests/lean/tst6.lean b/tests/lean/tst6.lean index e13f1eab9..ad4e17799 100644 --- a/tests/lean/tst6.lean +++ b/tests/lean/tst6.lean @@ -5,11 +5,11 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h Congr (Congr (Refl h) H1) H2 (* Display the theorem showing implicit arguments *) -Set lean::pp::implicit true +SetOption lean::pp::implicit true Show Environment 2 (* Display the theorem hiding implicit arguments *) -Set lean::pp::implicit false +SetOption lean::pp::implicit false Show Environment 2 Theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := @@ -20,7 +20,7 @@ Theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) (* Show proof of the last theorem with all implicit arguments *) -Set lean::pp::implicit true +SetOption lean::pp::implicit true Show Environment 1 (* Using placeholders to hide the type of H1 *) @@ -31,7 +31,7 @@ Theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h (fun H1 : _, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) -Set lean::pp::implicit true +SetOption lean::pp::implicit true Show Environment 1 (* Same example but the first conjuct has unnecessary stuff *) @@ -42,7 +42,7 @@ Theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ (fun H1 : _, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) -Set lean::pp::implicit false +SetOption lean::pp::implicit false Show Environment 1 Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) := @@ -54,5 +54,5 @@ Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC)) -Set lean::pp::implicit false +SetOption lean::pp::implicit false Show Environment 1 diff --git a/tests/lean/unicode.lean b/tests/lean/unicode.lean index 356b0a6b8..7e86bf989 100644 --- a/tests/lean/unicode.lean +++ b/tests/lean/unicode.lean @@ -1,8 +1,8 @@ Show true /\ false -Set pp::unicode false +SetOption pp::unicode false Show true /\ false -Set pp::unicode true -Set lean::pp::notation false +SetOption pp::unicode true +SetOption lean::pp::notation false Show true /\ false -Set pp::unicode false +SetOption pp::unicode false Show true /\ false diff --git a/tests/lua/front.lua b/tests/lua/front.lua index 19228e5b7..1d45eec71 100644 --- a/tests/lua/front.lua +++ b/tests/lua/front.lua @@ -8,8 +8,8 @@ Variables i j : Int Variables p q : Bool Notation 100 _ ++ _ : f Notation 100 _ ++ _ : g -Set pp::colors true -Set pp::width 300 +SetOption pp::colors true +SetOption pp::width 300 ]], env) print(get_options()) assert(get_options():get{"pp", "colors"}) diff --git a/tests/lua/parser2.lua b/tests/lua/parser2.lua index 94514100b..02d463449 100644 --- a/tests/lua/parser2.lua +++ b/tests/lua/parser2.lua @@ -3,14 +3,14 @@ parse_lean_cmds([[ Variable N : Type Variables x y : N Variable f : N -> N -> N - Set pp::colors false + SetOption pp::colors false ]], env) local f, x, y = Consts("f, x, y") print(env:check_type(f(x, y))) assert(env:check_type(f(x, y)) == Const("N")) assert(not get_options():get{"pp", "colors"}) parse_lean_cmds([[ - Set pp::colors true + SetOption pp::colors true ]], env) assert(get_options():get{"pp", "colors"}) local o = get_options() @@ -18,7 +18,7 @@ o:update({"lean", "pp", "notation"}, false) assert(not o:get{"lean", "pp", "notation"}) o = parse_lean_cmds([[ Check fun x : N, y - Set pp::notation true + SetOption pp::notation true Check fun x : N, y ]], env, o) print(o)