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

feat(frontends/lean/decl_cmds): avoid funny names when displaying error messages for "examples"

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-01 15:35:28 -07:00
parent b62e6bb133
commit b6fde68012
15 changed files with 32 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/frontends/lean/decl_cmds.cpp
View file

@ -910,9 +910,11 @@ class definition_cmd_fn {
buffer<name> m_ls_buffer_checkpoint; buffer<name> m_ls_buffer_checkpoint;
void save_checkpoint() { void save_checkpoint() {
m_type_checkpoint = m_type; if (m_kind != Example) {
m_env_checkpoint = m_env; m_type_checkpoint = m_type;
m_ls_buffer_checkpoint = m_ls_buffer; m_env_checkpoint = m_env;
m_ls_buffer_checkpoint = m_ls_buffer;
}
} }
bool is_definition() const { return m_kind == Definition || m_kind == Abbreviation || m_kind == LocalAbbreviation; } bool is_definition() const { return m_kind == Definition || m_kind == Abbreviation || m_kind == LocalAbbreviation; }
@ -921,7 +923,7 @@ class definition_cmd_fn {
void parse_name() { void parse_name() {
if (m_kind == Example) if (m_kind == Example)
m_name = m_p.mk_fresh_name(); m_name = name{"example"};
else else
m_name = m_p.check_id_next("invalid declaration, identifier expected"); m_name = m_p.check_id_next("invalid declaration, identifier expected");
} }
@ -1338,7 +1340,8 @@ static environment theorem_cmd(parser & p) {
return definition_cmd_core(p, Theorem, false, false); return definition_cmd_core(p, Theorem, false, false);
} }
static environment example_cmd(parser & p) { static environment example_cmd(parser & p) {
return definition_cmd_core(p, Example, false, false); definition_cmd_core(p, Example, false, false);
return p.env();
} }
static environment private_definition_cmd(parser & p) { static environment private_definition_cmd(parser & p) {
def_cmd_kind kind = Definition; def_cmd_kind kind = Definition;

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

@ -7,7 +7,7 @@ H : ∃ (n : ℕ), P n
P : ℕ → Prop, P : ℕ → Prop,
H : ∃ (n : ℕ), P n H : ∃ (n : ℕ), P n
⊢ ℕ ⊢ ℕ
571.lean:7:0: error: failed to add declaration '14.1' to environment, value has metavariables 571.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (P : …) (H : …), λ (P : …) (H : …),
?M_1 ?M_1

2
tests/lean/abbrev_paren.hlean.expected.out
View file

@ -1,7 +1,7 @@
abbrev_paren.hlean:5:54: error: don't know how to synthesize placeholder abbrev_paren.hlean:5:54: error: don't know how to synthesize placeholder
C : Precategory C : Precategory
⊢ C = Precategory.mk (carrier C) C ⊢ C = Precategory.mk (carrier C) C
abbrev_paren.hlean:5:54: error: failed to add declaration '14.0' to environment, value has metavariables abbrev_paren.hlean:5:54: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (C : Precategory), λ (C : Precategory),
?M_1 ?M_1

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

@ -8,7 +8,7 @@ a b : Prop
apply_fail.lean:4:0: error: don't know how to synthesize placeholder apply_fail.lean:4:0: error: don't know how to synthesize placeholder
a b : Prop a b : Prop
⊢ a ∧ b ⊢ a ∧ b
apply_fail.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables apply_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop), λ (a b : Prop),
?M_1 ?M_1

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

@ -7,7 +7,7 @@ assert_fail.lean:4:0: error: don't know how to synthesize placeholder
a b : Prop, a b : Prop,
H : b ∧ a H : b ∧ a
⊢ a ∧ b ⊢ a ∧ b
assert_fail.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables assert_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop) (H : …), λ (a b : Prop) (H : …),
?M_1 ?M_1
@ -18,7 +18,7 @@ assert_fail.lean:10:0: error: don't know how to synthesize placeholder
a : Prop, a : Prop,
Ha : a Ha : a
⊢ a ⊢ a
assert_fail.lean:10:0: error: failed to add declaration '14.1' to environment, value has metavariables assert_fail.lean:10:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : Prop) (Ha : a), λ (a : Prop) (Ha : a),
?M_1 ?M_1

10
tests/lean/constr_tac_errors.lean.expected.out
View file

@ -5,7 +5,7 @@ proof state:
constr_tac_errors.lean:4:0: error: don't know how to synthesize placeholder constr_tac_errors.lean:4:0: error: don't know how to synthesize placeholder
⊢ nat ⊢ nat
constr_tac_errors.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables constr_tac_errors.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
?M_1 ?M_1
constr_tac_errors.lean:12:2: error:invalid 'constructor' tactic, goal is an inductive datatype, but it does not have 2 constructor(s) constr_tac_errors.lean:12:2: error:invalid 'constructor' tactic, goal is an inductive datatype, but it does not have 2 constructor(s)
@ -17,7 +17,7 @@ Hb : b
constr_tac_errors.lean:13:0: error: don't know how to synthesize placeholder constr_tac_errors.lean:13:0: error: don't know how to synthesize placeholder
a b : Prop a b : Prop
⊢ a → b → a ∧ b ⊢ a → b → a ∧ b
constr_tac_errors.lean:13:0: error: failed to add declaration '14.2' to environment, value has metavariables constr_tac_errors.lean:13:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop), λ (a b : Prop),
?M_1 ?M_1
@ -30,7 +30,7 @@ Hb : b
constr_tac_errors.lean:19:0: error: don't know how to synthesize placeholder constr_tac_errors.lean:19:0: error: don't know how to synthesize placeholder
a b : Prop a b : Prop
⊢ a → b → a ∧ b ⊢ a → b → a ∧ b
constr_tac_errors.lean:19:0: error: failed to add declaration '14.3' to environment, value has metavariables constr_tac_errors.lean:19:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop), λ (a b : Prop),
?M_1 ?M_1
@ -43,7 +43,7 @@ Hb : b
constr_tac_errors.lean:32:0: error: don't know how to synthesize placeholder constr_tac_errors.lean:32:0: error: don't know how to synthesize placeholder
a b : Prop a b : Prop
⊢ a → b → unit ⊢ a → b → unit
constr_tac_errors.lean:32:0: error: failed to add declaration '14.5' to environment, value has metavariables constr_tac_errors.lean:32:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop), λ (a b : Prop),
?M_1 ?M_1
@ -54,6 +54,6 @@ proof state:
constr_tac_errors.lean:40:0: error: don't know how to synthesize placeholder constr_tac_errors.lean:40:0: error: don't know how to synthesize placeholder
⊢ nat → nat ⊢ nat → nat
constr_tac_errors.lean:40:0: error: failed to add declaration '14.7' to environment, value has metavariables constr_tac_errors.lean:40:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
?M_1 ?M_1

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

@ -18,7 +18,7 @@ a_2 : b
exact_partial.lean:5:0: error: don't know how to synthesize placeholder exact_partial.lean:5:0: error: don't know how to synthesize placeholder
a b : Prop a b : Prop
⊢ a → b → a ∧ b ⊢ a → b → a ∧ b
exact_partial.lean:5:0: error: failed to add declaration '14.0' to environment, value has metavariables exact_partial.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop), λ (a b : Prop),
?M_1 ?M_1

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

@ -15,7 +15,7 @@ a b c : nat,
h₁ : a = b, h₁ : a = b,
h₂ : b = c h₂ : b = c
⊢ a = c ⊢ a = c
exact_partial2.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables exact_partial2.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b c : nat) (h₁ : …) (h₂ : …), λ (a b c : nat) (h₁ : …) (h₂ : …),
?M_1 ?M_1

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

@ -9,7 +9,7 @@ quasireducible.lean:11:3: error: don't know how to synthesize placeholder
a : nat, a : nat,
H : f a = a H : f a = a
⊢ g a = a ⊢ g a = a
quasireducible.lean:11:3: error: failed to add declaration '14.1' to environment, value has metavariables quasireducible.lean:11:3: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : nat) (H : …), λ (a : nat) (H : …),
?M_1 ?M_1
@ -24,7 +24,7 @@ quasireducible.lean:16:3: error: don't know how to synthesize placeholder
a : nat, a : nat,
H : f a = a H : f a = a
⊢ g a = a ⊢ g a = a
quasireducible.lean:16:3: error: failed to add declaration '14.2' to environment, value has metavariables quasireducible.lean:16:3: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : nat) (H : …), λ (a : nat) (H : …),
?M_1 ?M_1

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

@ -1,4 +1,4 @@
red.lean:9:19: error: type mismatch at definition '14.1', has type red.lean:9:19: error: type mismatch at definition 'example', has type
f = f f = f
but is expected to have type but is expected to have type
f = g f = g

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

@ -9,7 +9,7 @@ A : Type,
n : nat, n : nat,
v : vector A n v : vector A n
⊢ v = v ⊢ v = v
revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, value has metavariables revert_fail.lean:6:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A : Type) (n : nat) (v : …), λ (A : Type) (n : nat) (v : …),
?M_1 ?M_1
@ -19,7 +19,7 @@ no goals
revert_fail.lean:12:0: error: don't know how to synthesize placeholder revert_fail.lean:12:0: error: don't know how to synthesize placeholder
n : nat n : nat
⊢ n = n ⊢ n = n
revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables revert_fail.lean:12:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (n : nat), λ (n : nat),
?M_1 ?M_1
@ -30,7 +30,7 @@ n : nat
revert_fail.lean:17:0: error: don't know how to synthesize placeholder revert_fail.lean:17:0: error: don't know how to synthesize placeholder
n : nat n : nat
⊢ n = n ⊢ n = n
revert_fail.lean:17:0: error: failed to add declaration '14.2' to environment, value has metavariables revert_fail.lean:17:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (n : nat), λ (n : nat),
?M_1 ?M_1

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

@ -11,7 +11,7 @@ a b : ℕ,
Ha : a = 0, Ha : a = 0,
Hb : b = 0 Hb : b = 0
⊢ a + b = 0 ⊢ a + b = 0
rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, value has metavariables rewrite_fail.lean:6:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : ℕ) (Ha : …) (Hb : …), λ (a b : ℕ) (Ha : …) (Hb : …),
?M_1 ?M_1
@ -21,7 +21,7 @@ no goals
rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder
a : ℕ a : ℕ
⊢ a = a ⊢ a = a
rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables rewrite_fail.lean:12:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : ℕ), λ (a : ℕ),
?M_1 ?M_1

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

@ -12,7 +12,7 @@ Hab : a ∧ b,
Ha : a, Ha : a,
Hb : b Hb : b
⊢ b ∧ a ⊢ b ∧ a
show_tac.lean:7:0: error: failed to add declaration '14.0' to environment, value has metavariables show_tac.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop) (Hab : …), λ (a b : Prop) (Hab : …),
?M_1 ?M_1

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

@ -15,7 +15,7 @@ a b c : nat,
H₁ : a = b, H₁ : a = b,
H₂ : b = c H₂ : b = c
⊢ a = c ⊢ a = c
unsolved_proof_qed.lean:2:0: error: failed to add declaration '14.0' to environment, value has metavariables unsolved_proof_qed.lean:2:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b c : nat) (H₁ : …) (H₂ : …), λ (a b c : nat) (H₁ : …) (H₂ : …),
?M_1 ?M_1
@ -36,7 +36,7 @@ a b c : nat,
H₁ : a = b, H₁ : a = b,
H₂ : b = c H₂ : b = c
⊢ c = a ⊢ c = a
unsolved_proof_qed.lean:5:0: error: failed to add declaration '14.1' to environment, value has metavariables unsolved_proof_qed.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b c : nat) (H₁ : …) (H₂ : …), λ (a b c : nat) (H₁ : …) (H₂ : …),
have aux : …, from ?M_1, have aux : …, from ?M_1,

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

@ -7,7 +7,7 @@ user_rec_crash.lean:4:0: error: don't know how to synthesize placeholder
a b : Prop, a b : Prop,
h : a ∧ b h : a ∧ b
⊢ a ⊢ a
user_rec_crash.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables user_rec_crash.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop) (h : …), λ (a b : Prop) (h : …),
?M_1 ?M_1