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

fix(frontends/lean): better error message for 'proof ... qed' blocks containing unsolved placeholders

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-20 15:50:37 -07:00
parent df05edf333
commit 107763a506
3 changed files with 50 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -278,7 +278,7 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
static expr parse_proof_qed_core(parser & p, pos_info const & pos) { static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
expr r = p.parse_expr(); expr r = p.parse_expr();
p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected"); p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected");
r = p.mk_by(p.mk_app(get_rexact_tac_fn(), r, pos), pos); r = p.mk_by(p.mk_app(get_exact_tac_fn(), r, pos), pos);
return r; return r;
} }

6
tests/lean/unsolved_proof_qed.lean Normal file
View file

@ -0,0 +1,6 @@
example (a b c : nat) (H₁ : a = b) (H₂ : b = c) : a = c :=
proof eq.trans H₁ _ qed
example (a b c : nat) (H₁ : a = b) (H₂ : b = c) : a = c :=
have aux : c = a, proof eq.trans _ (eq.symm H₁) qed,
(eq.symm aux)

43
tests/lean/unsolved_proof_qed.lean.expected.out Normal file
View file

@ -0,0 +1,43 @@
unsolved_proof_qed.lean:2:18: error: don't know how to synthesize placeholder
a b c : nat,
H₁ : a = b,
H₂ : b = c
⊢ b = c
unsolved_proof_qed.lean:2:0: error:invalid 'exact' tactic, term still contains metavariables after elaboration
eq.trans H₁ ?M_1
proof state:
a b c : nat,
H₁ : a = b,
H₂ : b = c
⊢ a = c
unsolved_proof_qed.lean:2:0: error: don't know how to synthesize placeholder
a b c : nat,
H₁ : a = b,
H₂ : b = c
⊢ a = c
unsolved_proof_qed.lean:2:0: error: failed to add declaration '14.0' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b c : nat) (H₁ : …) (H₂ : …),
?M_1
unsolved_proof_qed.lean:5:33: error: don't know how to synthesize placeholder
a b c : nat,
H₁ : a = b,
H₂ : b = c
⊢ c = b
unsolved_proof_qed.lean:5:18: error:invalid 'exact' tactic, term still contains metavariables after elaboration
eq.trans ?M_1 (eq.symm H₁)
proof state:
a b c : nat,
H₁ : a = b,
H₂ : b = c
⊢ c = a
unsolved_proof_qed.lean:5:18: error: don't know how to synthesize placeholder
a b c : nat,
H₁ : a = b,
H₂ : b = c
⊢ c = a
unsolved_proof_qed.lean:5:0: error: failed to add declaration '14.1' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b c : nat) (H₁ : …) (H₂ : …),
have aux : …, from ?M_1,
…