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

feat(frontends/lean/builtin_exprs): tolerate dangling ',' in begin-end block

Browse source 
This is useful when debugging proofs.
This commit is contained in:
Leonardo de Moura 2014-10-20 15:58:11 -07:00
parent a3aca96cb9
commit 9b8f60b739
2 changed files with 15 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -129,11 +129,8 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
first = false;
else
p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
if (p.curr_is_token(get_end_tk())) {
auto pos = p.pos();
p.next();
throw parser_error("invalid 'begin-end' expression, tactic or expression expected", pos);
}
if (p.curr_is_token(get_end_tk()))
break;
bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
p.curr_is_token(get_fun_tk()));

13
tests/lean/run/beginend2.lean Normal file
View file

@ -0,0 +1,13 @@
import hott.path tools.tactic
open path tactic
open path (induction_on)
definition concat_whisker2 {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
(whiskerR a q) @ (whiskerL p' b) ≈ (whiskerL p b) @ (whiskerR a q') :=
begin
apply (induction_on b),
apply (induction_on a),
apply ((concat_1p _)^),
end
exit