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

Modify verbose message for Set command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-02 12:29:21 -07:00
parent 0a67679afb
commit e218b92a9d
24 changed files with 42 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/lean_parser.cpp
View file

@ -1312,7 +1312,7 @@ class parser::imp {
} }
updt_options(); updt_options();
if (m_verbose) if (m_verbose)
regular(m_frontend) << " Set option: " << id << endl; regular(m_frontend) << " Set: " << id << endl;
} }
void parse_import() { void parse_import() {

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

@ -9,9 +9,9 @@ Int
Assumed: m Assumed: m
n + m n + m
n + x + m n + x + m
Set option: lean::pp::coercion Set: lean::pp::coercion
(nat_to_int n) + x + (nat_to_int m) + (nat_to_int 10) (nat_to_int n) + x + (nat_to_int m) + (nat_to_int 10)
x + (nat_to_int n) + (nat_to_int m) + (nat_to_int 10) x + (nat_to_int n) + (nat_to_int m) + (nat_to_int 10)
(nat_to_int (n + m + 10)) + x (nat_to_int (n + m + 10)) + x
Set option: lean::pp::notation Set: lean::pp::notation
Int::add (nat_to_int (Nat::add (Nat::add n m) 10)) x Int::add (nat_to_int (Nat::add (Nat::add n m) 10)) x

2
tests/lean/coercion1.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Assumed: T Assumed: T
Assumed: R Assumed: R
Assumed: f Assumed: f

12
tests/lean/coercion2.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Assumed: T Assumed: T
Assumed: R Assumed: R
Assumed: t2r Assumed: t2r
@ -9,23 +9,23 @@ g a a
Assumed: b Assumed: b
g a b g a b
g b a g b a
Set option: lean::pp::coercion Set: lean::pp::coercion
g (t2r a) (t2r a) g (t2r a) (t2r a)
g (t2r a) b g (t2r a) b
g b (t2r a) g b (t2r a)
Set option: lean::pp::coercion Set: lean::pp::coercion
Assumed: S Assumed: S
Assumed: s Assumed: s
Assumed: r Assumed: r
Assumed: h Assumed: h
Set option: lean::pp::notation Set: lean::pp::notation
g (g a b) a g (g a b) a
h (h r s) r h (h r s) r
R R
S S
Set option: lean::pp::coercion Set: lean::pp::coercion
g (g (t2r a) b) (t2r a) g (g (t2r a) b) (t2r a)
h (h r s) r h (h r s) r
Set option: lean::pp::notation Set: lean::pp::notation
(t2r a) ++ b ++ (t2r a) (t2r a) ++ b ++ (t2r a)
r ++ s ++ r r ++ s ++ r

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

File diff suppressed because one or more lines are too long

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

@ -1,6 +1,6 @@
Set option: pp::colors Set: pp::colors
⊤ ⊤
Set option: lean::pp::notation Set: lean::pp::notation
and true false and true false
Assumed: a Assumed: a
Error (line: 8, 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'
@ -17,5 +17,5 @@ Variable A : Type
⟨lean::pp::notation ↦ false, pp::colors ↦ false⟩ ⟨lean::pp::notation ↦ false, pp::colors ↦ false⟩
Error (line: 15, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options Error (line: 15, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
Error (line: 16, pos: 23) invalid option value, given option is not an integer Error (line: 16, pos: 23) invalid option value, given option is not an integer
Set option: lean::pp::notation Set: lean::pp::notation
a ∧ b a ∧ b

2
tests/lean/ex3.lean.expected.out
View file

@ -9,7 +9,7 @@ expected type
given type given type
T T
Assumed: myeq2 Assumed: myeq2
Set option: lean::pp::implicit Set: lean::pp::implicit
Error (line: 9, pos: 15) type mismatch at application argument 3 of Error (line: 9, pos: 15) type mismatch at application argument 3 of
myeq2::explicit Bool ⊤ a myeq2::explicit Bool ⊤ a
expected type expected type

2
tests/lean/overload1.lean.expected.out
View file

@ -2,7 +2,7 @@
Assumed: f Assumed: f
Assumed: g Assumed: g
⊤ ++ ⊥ ++ ⊤ ⊤ ++ ⊥ ++ ⊤
Set option: lean::pp::notation Set: lean::pp::notation
f (f true false) true f (f true false) true
Assumed: a Assumed: a
Assumed: b Assumed: b

2
tests/lean/tst1.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Assumed: N Assumed: N
Assumed: lt Assumed: lt
Assumed: zero Assumed: zero

2
tests/lean/tst10.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Assumed: a Assumed: a
Assumed: b Assumed: b
a ∧ b a ∧ b

2
tests/lean/tst11.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Defined: xor Defined: xor
⊤ ⊕ ⊥ ⊤ ⊕ ⊥
⊥ ⊥

2
tests/lean/tst12.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
λ x y : Bool, x ∧ y λ x y : Bool, x ∧ y
let x := ⊤, let x := ⊤,
y := ⊤, y := ⊤,

2
tests/lean/tst13.lean.expected.out
View file

@ -1,3 +1,3 @@
Set option: pp::colors Set: pp::colors
λ x x : Bool, x λ x x : Bool, x
let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z

2
tests/lean/tst14.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Int → Int → Int Int → Int → Int
Assumed: f Assumed: f
f 0 f 0

2
tests/lean/tst15.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Assumed: x Assumed: x
Type U+3 ⊔ M+2 ⊔ 3 Type U+3 ⊔ M+2 ⊔ 3
Assumed: f Assumed: f

2
tests/lean/tst16.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Assumed: f Assumed: f
∀ a b : Type, (f a) = (f b) ∀ a b : Type, (f a) = (f b)
Assumed: g Assumed: g

2
tests/lean/tst17.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Assumed: f Assumed: f
Assumed: g Assumed: g
∀ a b : Type, ∃ c : Type, (g a b) = (f c) ∀ a b : Type, ∃ c : Type, (g a b) = (f c)

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

@ -2,11 +2,11 @@
Assumed: a Assumed: a
Assumed: b Assumed: b
a ∧ b a ∧ b
Set option: lean::pp::notation Set: lean::pp::notation
⟨lean::pp::notation ↦ false⟩ ⟨lean::pp::notation ↦ false⟩
and a b and a b
Variable a : Bool Variable a : Bool
Variable b : Bool Variable b : Bool
Set option: lean::pp::notation Set: lean::pp::notation
⟨lean::pp::notation ↦ true⟩ ⟨lean::pp::notation ↦ true⟩
a ∧ b a ∧ b

2
tests/lean/tst3.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Notation 10 if _ then _ : implies Notation 10 if _ then _ : implies
if ⊤ then ⊥ if ⊤ then ⊥
if ⊤ then (if a then ⊥) if ⊤ then (if a then ⊥)

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

@ -2,11 +2,11 @@
Assumed: N Assumed: N
Assumed: n1 Assumed: n1
Assumed: n2 Assumed: n2
Set option: lean::pp::implicit Set: lean::pp::implicit
f::explicit N n1 n2 f::explicit N n1 n2
f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y) f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
Assumed: EqNice Assumed: EqNice
Set option: pp::colors Set: pp::colors
EqNice::explicit N n1 n2 EqNice::explicit N n1 n2
N N
Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b) Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b)

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

@ -1,10 +1,10 @@
Set option: pp::colors Set: pp::colors
Assumed: N Assumed: N
Assumed: a Assumed: a
Assumed: b Assumed: b
a ≃ b a ≃ b
Bool Bool
Set option: lean::pp::implicit Set: lean::pp::implicit
heq::explicit N a b heq::explicit N a b
heq::explicit Type 2 Type 1 Type 1 heq::explicit Type 2 Type 1 Type 1
heq::explicit Bool ⊤ ⊥ heq::explicit Bool ⊤ ⊥

14
tests/lean/tst6.lean.expected.out
View file

@ -1,8 +1,8 @@
Set option: pp::colors Set: pp::colors
Assumed: N Assumed: N
Assumed: h Assumed: h
Proved: CongrH Proved: CongrH
Set option: lean::pp::implicit Set: lean::pp::implicit
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
Congr::explicit Congr::explicit
N N
@ -15,11 +15,11 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h
H2 H2
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
CongrH::explicit a1 a2 b1 b2 H1 H2 CongrH::explicit a1 a2 b1 b2 H1 H2
Set option: lean::pp::implicit Set: lean::pp::implicit
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 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
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2 Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
Proved: Example1 Proved: Example1
Set option: lean::pp::implicit Set: lean::pp::implicit
Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) := Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
DisjCases::explicit DisjCases::explicit
(a = b ∧ b = c) (a = b ∧ b = c)
@ -55,7 +55,7 @@ Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
(Conjunct2::explicit (a = d) (d = c) H1)) (Conjunct2::explicit (a = d) (d = c) H1))
(Refl::explicit N b)) (Refl::explicit N b))
Proved: Example2 Proved: Example2
Set option: lean::pp::implicit Set: lean::pp::implicit
Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) := Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
DisjCases::explicit DisjCases::explicit
(a = b ∧ b = c) (a = b ∧ b = c)
@ -91,14 +91,14 @@ Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
(Conjunct2::explicit (a = d) (d = c) H1)) (Conjunct2::explicit (a = d) (d = c) H1))
(Refl::explicit N b)) (Refl::explicit N b))
Proved: Example3 Proved: Example3
Set option: lean::pp::implicit Set: lean::pp::implicit
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) := 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 DisjCases
H H
(λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b)) (λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b))
(λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) (λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
Proved: Example4 Proved: Example4
Set option: lean::pp::implicit Set: lean::pp::implicit
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) := 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) :=
DisjCases DisjCases
H H

2
tests/lean/tst7.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Assumed: f Assumed: f
λ (A B : Type) (a : B), f B a λ (A B : Type) (a : B), f B a
Error (line: 5, pos: 40) application type mismatch during term elaboration at term Error (line: 5, pos: 40) application type mismatch during term elaboration at term

2
tests/lean/tst8.lean.expected.out
View file

@ -1,4 +1,4 @@
Set option: pp::colors Set: pp::colors
Π (A : Type) (a : A), A Π (A : Type) (a : A), A
Assumed: g Assumed: g
Defined: f Defined: f