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

chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-05 21:45:31 -08:00
parent 7222a2d1a9
commit 8c956280d9
63 changed files with 170 additions and 169 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
doc/lean/expr.md
View file

@ -89,16 +89,16 @@ infix 50 = : eq
```
The curly braces indicate that the first argument of `eq` is implicit. The symbol `=` is just a syntax sugar for `eq`.
In the following example, we use the `setoption` command to force Lean to display implicit arguments and
In the following example, we use the `set::option` command to force Lean to display implicit arguments and
disable notation when pretty printing expressions.
```lean
setoption pp::implicit true
setoption pp::notation false
set::option pp::implicit true
set::option pp::notation false
check 1 = 2
-- restore default configuration
setoption pp::implicit false
setoption pp::notation true
set::option pp::implicit false
set::option pp::notation true
check 1 = 2
```

2
examples/lean/even.lean
View file

@ -63,7 +63,7 @@ print environment 2.
-- By default, Lean does not display implicit arguments.
-- The following command will force it to display them.
setoption pp::implicit true.
set::option pp::implicit true.
print environment 2.

4
examples/lean/ex1.lean
View file

@ -30,6 +30,6 @@ theorem T2 : (h a (h a b)) = (h a (h c e)) :=
print environment 2
-- print implicit arguments
setoption lean::pp::implicit true
setoption pp::width 150
set::option lean::pp::implicit true
set::option pp::width 150
print environment 2

2
examples/lean/ex2.lean
View file

@ -6,7 +6,7 @@ theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r
P_qr := and::elimr H_pq_qr
in P_qr ◂ (P_pq ◂ H_p)
setoption pp::implicit true.
set::option pp::implicit true.
print environment 1.
theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c

20
src/builtin/Int.lean
View file

@ -46,14 +46,14 @@ infix 50 | : divides
definition abs (a : Int) : Int := if (0 ≤ a) a (- a)
notation 55 | _ | : abs
setopaque sub true
setopaque neg true
setopaque mod true
setopaque divides true
setopaque abs true
setopaque ge true
setopaque lt true
setopaque gt true
set::opaque sub true
set::opaque neg true
set::opaque mod true
set::opaque divides true
set::opaque abs true
set::opaque ge true
set::opaque lt true
set::opaque gt true
end
namespace Nat
@ -63,6 +63,6 @@ infixl 65 - : sub
definition neg (a : Nat) : Int := - (nat_to_int a)
notation 75 - _ : neg
setopaque sub true
setopaque neg true
set::opaque sub true
set::opaque neg true
end

8
src/builtin/Nat.lean
View file

@ -243,8 +243,8 @@ theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
... = a + w1 : { symm L2 }
... = b : Hw1
setopaque ge true
setopaque lt true
setopaque gt true
setopaque id true
set::opaque ge true
set::opaque lt true
set::opaque gt true
set::opaque id true
end

12
src/builtin/kernel.lean
View file

@ -240,11 +240,11 @@ theorem exists::intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A
-- them as opaque Opaque definitions improve performance, and
-- effectiveness of Lean's elaborator
setopaque implies true
setopaque not true
setopaque or true
setopaque and true
setopaque forall true
set::opaque implies true
set::opaque not true
set::opaque or true
set::opaque and true
set::opaque forall true
theorem or::comm (a b : Bool) : (a ∨ b) == (b ∨ a)
:= iff::intro (assume H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a))
@ -393,4 +393,4 @@ theorem exists::unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) =
:= iff::intro (assume H : (∃ x : A, P x), exists::unfold1 a H)
(assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists::unfold2 a H)
setopaque exists true
set::opaque exists true

47
src/frontends/lean/parser_cmds.cpp
View file

@ -37,8 +37,8 @@ static name g_infix_kwd("infix");
static name g_infixl_kwd("infixl");
static name g_infixr_kwd("infixr");
static name g_notation_kwd("notation");
static name g_set_option_kwd("setoption");
static name g_set_opaque_kwd("setopaque");
static name g_set_option_kwd("set", "option");
static name g_set_opaque_kwd("set", "opaque");
static name g_options_kwd("options");
static name g_env_kwd("environment");
static name g_import_kwd("import");
@ -596,28 +596,29 @@ void parser_imp::parse_help() {
}
} else {
regular(m_io_state) << "Available commands:" << endl
<< " alias [id] : [expr] define an alias for the given expression" << endl
<< " axiom [id] : [type] assert/postulate a new axiom" << endl
<< " check [expr] type check the given expression" << endl
<< " alias [id] : [expr] define an alias for the given expression" << endl
<< " axiom [id] : [type] assert/postulate a new axiom" << endl
<< " check [expr] type check the given expression" << endl
<< " definition [id] : [type] := [expr] define a new element" << endl
<< " end end the current scope/namespace" << endl
<< " eval [expr] evaluate the given expression" << endl
<< " exit exit" << endl
<< " help display this message" << endl
<< " help options display available options" << endl
<< " help notation describe commands for defining infix, mixfix, postfix operators" << endl
<< " import [string] load the given file" << endl
<< " pop::scope discard the current scope" << endl
<< " print [expr] pretty print the given expression" << endl
<< " print Options print current the set of assigned options" << endl
<< " print [string] print the given string" << endl
<< " print Environment print objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
<< " print Environment [num] show the last num objects in the environment" << endl
<< " scope create a scope" << endl
<< " setoption [id] [value] set option [id] with value [value]" << endl
<< " theorem [id] : [type] := [expr] define a new theorem" << endl
<< " variable [id] : [type] declare/postulate an element of the given type" << endl
<< " universe [id] [level] declare a new universe variable that is >= the given level" << endl;
<< " end end the current scope/namespace" << endl
<< " eval [expr] evaluate the given expression" << endl
<< " exit exit" << endl
<< " help display this message" << endl
<< " help options display available options" << endl
<< " help notation describe commands for defining infix, mixfix, postfix operators" << endl
<< " import [string] load the given file" << endl
<< " pop::scope discard the current scope" << endl
<< " print [expr] pretty print the given expression" << endl
<< " print Options print current the set of assigned options" << endl
<< " print [string] print the given string" << endl
<< " print Environment print objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
<< " print Environment [num] show the last num objects in the environment" << endl
<< " scope create a scope" << endl
<< " set::option [id] [value] set option [id] with value [value]" << endl
<< " set::opaque [id] [bool] set the given definition as opaque/transparent" << endl
<< " theorem [id] : [type] := [expr] define a new theorem" << endl
<< " variable [id] : [type] declare/postulate an element of the given type" << endl
<< " universe [id] [level] declare a new universe variable that is >= the given level" << endl;
#if !defined(LEAN_WINDOWS)
regular(m_io_state) << "Type Ctrl-D to exit" << endl;
#endif

2
src/kernel/environment.cpp
View file

@ -33,7 +33,7 @@ class set_opaque_command : public neutral_object_cell {
public:
set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {}
virtual ~set_opaque_command() {}
virtual char const * keyword() const { return "setopaque"; }
virtual char const * keyword() const { return "set::opaque"; }
virtual void write(serializer & s) const { s << "Opa" << m_obj_name << m_opaque; }
name const & get_obj_name() const { return m_obj_name; }
bool get_flag() const { return m_opaque; }

10
src/tests/frontends/lean/parser.cpp
View file

@ -94,11 +94,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, "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, "set::option pp::indent true");
parse(env, ios, "set::option pp::indent 10");
parse_error(env, ios, "set::option pp::colors foo");
parse_error(env, ios, "set::option pp::colors \"foo\"");
parse(env, ios, "set::option 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.");

2
tests/lean/abst.lean
View file

@ -2,5 +2,5 @@ import Int.
axiom PlusComm(a b : Int) : a + b == b + a.
variable a : Int.
check (abst (fun x : Int, (PlusComm a x))).
setoption pp::implicit true.
set::option pp::implicit true.
check (abst (fun x : Int, (PlusComm a x))).

6
tests/lean/alias2.lean
View file

@ -3,14 +3,14 @@ scope
alias ℕℕ : Natural.
variable x : Natural.
print environment 1.
setoption pp::unicode false.
set::option pp::unicode false.
print environment 1.
setoption pp::unicode true.
set::option pp::unicode true.
print environment 1.
alias NN : Natural.
print environment 2.
alias ℕℕℕ : Natural.
print environment 3.
setoption pp::unicode false.
set::option pp::unicode false.
print environment 3.
pop::scope

4
tests/lean/arith1.lean
View file

@ -10,9 +10,9 @@ variable n : Nat
variable m : Nat
print n + m
print n + x + m
setoption lean::pp::coercion true
set::option lean::pp::coercion true
print n + x + m + 10
print x + n + m + 10
print n + m + 10 + x
setoption lean::pp::notation false
set::option lean::pp::notation false
print n + m + 10 + x

2
tests/lean/arith2.lean
View file

@ -7,7 +7,7 @@ variable x : Real
variable i : Int
variable n : Nat
print x + i + 1 + n
setoption lean::pp::coercion true
set::option lean::pp::coercion true
print x + i + 1 + n
print x * i + x
print x - i + x - x >= 0

2
tests/lean/arith3.lean
View file

@ -4,7 +4,7 @@ eval 8 div 4
eval 7 div 3
eval 7 mod 3
print -8 mod 3
setoption lean::pp::notation false
set::option lean::pp::notation false
print -8 mod 3
eval -8 mod 3
eval (-8 div 3)*3 + (-8 mod 3)

4
tests/lean/arith6.lean
View file

@ -1,5 +1,5 @@
import Int.
setoption pp::unicode false
set::option pp::unicode false
print 3 | 6
eval 3 | 6
eval 3 | 7
@ -9,5 +9,5 @@ variable x : Int
eval x | 3
eval 3 | x
eval 6 | 3
setoption pp::notation false
set::option pp::notation false
print 3 | x

2
tests/lean/arith7.lean
View file

@ -11,6 +11,6 @@ eval |x + 1| > 0
variable y : Int
eval |x + y|
print |x + y| > x
setoption pp::notation false
set::option pp::notation false
print |x + y| > x
print |x + y| + |y + x| > x

4
tests/lean/bad10.lean
View file

@ -1,5 +1,5 @@
setoption pp::implicit true.
setoption pp::colors false.
set::option pp::implicit true.
set::option pp::colors false.
variable N : Type.
definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ :=

4
tests/lean/bad2.lean
View file

@ -8,6 +8,6 @@ definition n3 : list Int := cons 10 nil
definition n4 : list Int := nil
definition n5 : _ := cons 10 nil
setoption pp::coercion true
setoption pp::implicit true
set::option pp::coercion true
set::option pp::implicit true
print environment 1.

4
tests/lean/bad9.lean
View file

@ -1,5 +1,5 @@
setoption pp::implicit true.
setoption pp::colors false.
set::option pp::implicit true.
set::option pp::colors false.
variable N : Type.
check

2
tests/lean/cast2.lean
View file

@ -7,6 +7,6 @@ axiom H : (A -> B) = (A' -> B')
variable a : A
check dominj H
theorem BeqB' : B = B' := raninj H a
setoption pp::implicit true
set::option pp::implicit true
print dominj H
print raninj H a

2
tests/lean/cast4.lean
View file

@ -1,5 +1,5 @@
import cast
setoption pp::colors false
set::option pp::colors false
check fun (A A': TypeM)
(B : A -> TypeM)

10
tests/lean/coercion2.lean
View file

@ -8,25 +8,25 @@ print g a a
variable b : R
print g a b
print g b a
setoption lean::pp::coercion true
set::option lean::pp::coercion true
print g a a
print g a b
print g b a
setoption lean::pp::coercion false
set::option lean::pp::coercion false
variable S : Type
variable s : S
variable r : S
variable h : S -> S -> S
infixl 10 ++ : g
infixl 10 ++ : h
setoption lean::pp::notation false
set::option lean::pp::notation false
print a ++ b ++ a
print r ++ s ++ r
check a ++ b ++ a
check r ++ s ++ r
setoption lean::pp::coercion true
set::option lean::pp::coercion true
print a ++ b ++ a
print r ++ s ++ r
setoption lean::pp::notation true
set::option lean::pp::notation true
print a ++ b ++ a
print r ++ s ++ r

6
tests/lean/config.lean
View file

@ -1,3 +1,3 @@
-- setoption default configuration for tests
setoption pp::colors false
setoption pp::unicode true
-- set::option default configuration for tests
set::option pp::colors false
set::option pp::unicode true

2
tests/lean/elab4.lean
View file

@ -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
setoption pp::implicit true
set::option pp::implicit true
print environment 7.

2
tests/lean/elab5.lean
View file

@ -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
setoption pp::implicit true
set::option pp::implicit true
print environment 7.

2
tests/lean/elab7.lean
View file

@ -17,5 +17,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)))
print environment 4
setoption pp::implicit true
set::option pp::implicit true
print environment 4

2
tests/lean/eq1.lean
View file

@ -1,5 +1,5 @@
import Int.
variable i : Int
check i = 0
setoption pp::coercion true
set::option pp::coercion true
check i = 0

2
tests/lean/eq2.lean
View file

@ -4,5 +4,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.
setoption pp::implicit true
set::option pp::implicit true
check l = nil.

2
tests/lean/eq3.lean
View file

@ -6,5 +6,5 @@ variable v3 : Vector (0 + n)
axiom H1 : v1 == v2
axiom H2 : v2 == v3
check htrans H1 H2
setoption pp::implicit true
set::option pp::implicit true
check htrans H1 H2

10
tests/lean/ex2.lean
View file

@ -1,8 +1,8 @@
-- comment
print true
setoption lean::pp::notation false
set::option lean::pp::notation false
print true && false
setoption pp::unicode false
set::option pp::unicode false
print true && false
variable a : Bool
variable a : Bool
@ -12,7 +12,7 @@ variable A : Type
check a && A
print environment 1
print options
setoption lean::p::notation true
setoption lean::pp::notation 10
setoption lean::pp::notation true
set::option lean::p::notation true
set::option lean::pp::notation 10
set::option lean::pp::notation true
print a && b

4
tests/lean/ex2.lean.expected.out
View file

@ -19,7 +19,7 @@ Arguments types:
A : Type
variable A : Type
(lean::pp::notation := false, pp::unicode := false, pp::colors := false)
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
Error (line: 15, pos: 12) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
Error (line: 16, pos: 31) invalid option value, given option is not an integer
Set: lean::pp::notation
a /\ b

2
tests/lean/ex3.lean
View file

@ -5,5 +5,5 @@ variable a : T
check myeq _ true a
variable myeq2 {A:Type} (a b : A) : Bool
infix 50 === : myeq2
setoption lean::pp::implicit true
set::option lean::pp::implicit true
check true === a

2
tests/lean/exists3.lean
View file

@ -1,7 +1,7 @@
import Int.
variable P : Int -> Int -> Bool
setopaque exists false.
set::opaque exists false.
theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
forall::intro (fun a,

8
tests/lean/exists7.lean
View file

@ -1,11 +1,11 @@
setoption pp::colors false
set::option pp::colors false
variable N : Type
variables a b c : N
variables P : N -> N -> N -> Bool
setopaque forall false.
setopaque exists false.
setopaque not false.
set::opaque forall false.
set::opaque exists false.
set::opaque not false.
theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H))

2
tests/lean/implicit1.lean
View file

@ -6,7 +6,7 @@ print forall a b, f a b > 0
variable g : Int -> Real -> Int
print forall a b, g a b > 0
print forall a b, g a (f a b) > 0
setoption pp::coercion true
set::option pp::coercion true
print forall a b, g a (f a b) > 0
print fun a, a + 1
print fun a b, a + b

2
tests/lean/implicit2.lean
View file

@ -8,6 +8,6 @@ check g 10 20 true
check let r : Real -> Real -> Real := g 10 20
in r
check g 10
setoption pp::implicit true
set::option pp::implicit true
check let r : Real -> Real -> Real := g 10 20
in r

4
tests/lean/implicit3.lean
View file

@ -5,7 +5,7 @@ variable f : Int -> Int -> Int
variable g : Int -> Int -> Int -> Int
notation 10 _ ++ _ : f
notation 10 _ ++ _ : g
setoption pp::implicit true
setoption pp::notation false
set::option pp::implicit true
set::option pp::notation false
print (10 ++ 20)
print (10 ++ 20) 10

4
tests/lean/implicit6.lean
View file

@ -4,8 +4,8 @@ infixl 65 + : f
print true + false
print 10 + 20
print 10 + (- 20)
setoption pp::notation false
setoption pp::coercion true
set::option pp::notation false
set::option pp::coercion true
print true + false
print 10 + 20
print 10 + (- 20)

4
tests/lean/implicit7.lean
View file

@ -4,9 +4,9 @@ notation 100 _ ; _ ; _ : f
notation 100 _ ; _ ; _ : g
check 10 ; true ; false
check 10 ; 10 ; true
setoption pp::notation false
set::option pp::notation false
check 10 ; true ; false
check 10 ; 10 ; true
setoption pp::implicit true
set::option pp::implicit true
check 10 ; true ; false
check 10 ; 10 ; true

6
tests/lean/interactive/config.lean
View file

@ -1,3 +1,3 @@
-- setoption default configuration for tests
setoption pp::colors false
setoption pp::unicode true
-- set::option default configuration for tests
set::option pp::colors false
set::option pp::unicode true

2
tests/lean/interactive/t8.lean
View file

@ -1,5 +1,5 @@
(* import("tactic.lua") *)
setoption tactic::proof_state::goal_names true.
set::option tactic::proof_state::goal_names true.
theorem T (a : Bool) : a => a /\ a.
apply discharge.
apply and::intro.

2
tests/lean/let1.lean
View file

@ -6,5 +6,5 @@ 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
setoption pp::coercion true
set::option pp::coercion true
print let a : Int := 20 in a + 10

4
tests/lean/let3.lean
View file

@ -2,8 +2,8 @@ import Int.
variable magic : Pi (H : Bool), H
setoption pp::notation false
setoption pp::coercion true
set::option pp::notation false
set::option pp::coercion true
print let a : Int := 1,
H : a > 0 := magic (a > 0)
in H

2
tests/lean/let4.lean
View file

@ -41,7 +41,7 @@ let a := 10,
v2 : vector Int a := v1
in v2
setoption pp::coercion true
set::option pp::coercion true
print
let a := 10,

2
tests/lean/lua6.lean
View file

@ -1,6 +1,6 @@
import Int.
variable x : Int
setoption pp::notation false
set::option pp::notation false
(*
print(get_options())
*)

2
tests/lean/norm_bug1.lean
View file

@ -1,5 +1,5 @@
import cast
setoption pp::colors false
set::option pp::colors false
check fun (A A': TypeM)
(a : A)

6
tests/lean/norm_tac.lean
View file

@ -1,8 +1,8 @@
import Int
import tactic
setoption pp::implicit true
setoption pp::coercion true
setoption pp::notation false
set::option pp::implicit true
set::option pp::coercion true
set::option pp::notation false
variable vector (A : Type) (sz : Nat) : Type
variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
variable V1 : vector Int 10

2
tests/lean/overload1.lean
View file

@ -4,7 +4,7 @@ variable g : N -> N -> N
infixl 10 ++ : f
infixl 10 ++ : g
print true ++ false ++ true
setoption lean::pp::notation false
set::option lean::pp::notation false
print true ++ false ++ true
variable a : N
variable b : N

4
tests/lean/overload2.lean
View file

@ -10,8 +10,8 @@ coercion t2r
variable f : T -> R -> T
variable a : T
variable b : R
setoption lean::pp::coercion true
setoption lean::pp::notation false
set::option lean::pp::coercion true
set::option lean::pp::notation false
print f a b
print f b a
variable g : R -> T -> R

2
tests/lean/showenv.l
View file

@ -1,3 +1,3 @@
setoption pp::colors false
set::option pp::colors false
print "===BEGIN ENVIRONMENT==="
print environment

6
tests/lean/slow/config.lean
View file

@ -1,3 +1,3 @@
-- setoption default configuration for tests
setoption pp::colors false
setoption pp::unicode true
-- set::option default configuration for tests
set::option pp::colors false
set::option pp::unicode true

4
tests/lean/slow/deep.lean
View file

@ -3,6 +3,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.
setoption pp::width 80.
setoption lean::pp::max_depth 2000.
set::option pp::width 80.
set::option lean::pp::max_depth 2000.
eval f3 f 0.

6
tests/lean/subst.lean
View file

@ -4,7 +4,7 @@ variable n : Nat
axiom H1 : a + a + a = 10
axiom H2 : a = n
theorem T : a + n + a = 10 := subst H1 H2
setoption pp::coercion true
setoption pp::notation false
setoption pp::implicit true
set::option pp::coercion true
set::option pp::notation false
set::option pp::implicit true
print environment 1.

4
tests/lean/tst2.lean
View file

@ -2,10 +2,10 @@ print options
variable a : Bool
variable b : Bool
print a/\b
setoption lean::pp::notation false
set::option lean::pp::notation false
print options
print a/\b
print environment 2
setoption lean::pp::notation true
set::option lean::pp::notation true
print options
print a/\b

24
tests/lean/tst3.lean
View file

@ -1,10 +1,10 @@
setoption lean::parser::verbose false.
set::option lean::parser::verbose false.
notation 10 if _ then _ : implies.
print environment 1.
print if true then false.
variable a : Bool.
print if true then if a then false.
setoption lean::pp::notation false.
set::option lean::pp::notation false.
print 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.
print c |- d ; e.
setoption lean::pp::notation true.
set::option lean::pp::notation true.
print c |- d ; e.
variable fact : A -> A.
notation 20 _ ! : fact.
print c! !.
setoption lean::pp::notation false.
set::option lean::pp::notation false.
print c! !.
setoption lean::pp::notation true.
set::option lean::pp::notation true.
variable g : A -> A -> A.
notation 30 [ _ ; _ ] : g
print [c;d].
print [c ; [d;e] ].
setoption lean::pp::notation false.
set::option lean::pp::notation false.
print [c ; [d;e] ].
setoption lean::pp::notation true.
set::option lean::pp::notation true.
variable h : A -> A -> A.
notation 40 _ << _ >> : h.
print environment 1.
print d << e >>.
print [c ; d << e >> ].
setoption lean::pp::notation false.
set::option lean::pp::notation false.
print [c ; d << e >> ].
setoption lean::pp::notation true.
set::option 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.
print p1 || p2 && p3.
setoption lean::pp::notation false.
set::option lean::pp::notation false.
print c ** d ++ e ** c.
print p1 || p2 && p3.
setoption lean::pp::notation true.
set::option lean::pp::notation true.
print c = d || d = c.
print not p1 || p2.
print p1 && p3 || p2 && p3.
setoption lean::pp::notation false.
set::option lean::pp::notation false.
print not p1 || p2.
print p1 && p3 || p2 && p3.

2
tests/lean/tst4.lean
View file

@ -2,7 +2,7 @@ variable f {A : Type} (a b : A) : A
variable N : Type
variable n1 : N
variable n2 : N
setoption lean::pp::implicit true
set::option lean::pp::implicit true
print f n1 n2
print f (fun x : N -> N, x) (fun y : _, y)
variable EqNice {A : Type} (lhs rhs : A) : Bool

2
tests/lean/tst5.lean
View file

@ -3,7 +3,7 @@ variable a : N
variable b : N
print a = b
check a = b
setoption lean::pp::implicit true
set::option lean::pp::implicit true
print a = b
print (Type 1) = (Type 1)
print true = false

12
tests/lean/tst6.lean
View file

@ -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
setoption lean::pp::implicit true
set::option lean::pp::implicit true
print environment 2
-- Display the theorem hiding implicit arguments
setoption lean::pp::implicit false
set::option lean::pp::implicit false
print 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 (and::eliml H1) (and::elimr H1)) (refl b))
-- print proof of the last theorem with all implicit arguments
setoption lean::pp::implicit true
set::option lean::pp::implicit true
print 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 (and::eliml H1) (and::elimr H1)) (refl b))
setoption lean::pp::implicit true
set::option lean::pp::implicit true
print 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 (and::eliml H1) (and::elimr H1)) (refl b))
setoption lean::pp::implicit false
set::option lean::pp::implicit false
print 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 (and::eliml H1) (and::elimr H1)
in congrH AeqC (symm AeqC))
setoption lean::pp::implicit false
set::option lean::pp::implicit false
print environment 1

2
tests/lean/type_inf_bug1.lean
View file

@ -1,5 +1,5 @@
import cast
setoption pp::colors false
set::option pp::colors false
check fun (A A': TypeM)
(a : A)

8
tests/lean/unicode.lean
View file

@ -1,8 +1,8 @@
print true /\ false
setoption pp::unicode false
set::option pp::unicode false
print true /\ false
setoption pp::unicode true
setoption lean::pp::notation false
set::option pp::unicode true
set::option lean::pp::notation false
print true /\ false
setoption pp::unicode false
set::option pp::unicode false
print true /\ false

4
tests/lua/front.lua
View file

@ -10,8 +10,8 @@ variables i j : Int
variables p q : Bool
notation 100 _ ++ _ : f
notation 100 _ ++ _ : g
setoption pp::colors true
setoption pp::width 300
set::option pp::colors true
set::option pp::width 300
]], env)
print(get_options())
assert(get_options():get{"pp", "colors"})

6
tests/lua/parser2.lua
View file

@ -4,14 +4,14 @@ parse_lean_cmds([[
variable N : Type
variables x y : N
variable f : N -> N -> N
setoption pp::colors false
set::option pp::colors false
]], env)
local f, x, y = Consts("f, x, y")
print(env:type_check(f(x, y)))
assert(env:type_check(f(x, y)) == Const("N"))
assert(not get_options():get{"pp", "colors"})
parse_lean_cmds([[
setoption pp::colors true
set::option pp::colors true
]], env)
assert(get_options():get{"pp", "colors"})
local o = get_options()
@ -19,7 +19,7 @@ o:update({"lean", "pp", "notation"}, false)
assert(not o:get{"lean", "pp", "notation"})
o = parse_lean_cmds([[
check fun x : N, y
setoption pp::notation true
set::option pp::notation true
check fun x : N, y
]], env, o)
print(o)