max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/brackets): fixes #1703

Browse source
This commit is contained in:
Leonardo de Moura 2017-06-26 12:52:52 -07:00
parent 8ccdf350de
commit f339f97975
2 changed files with 17 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/brackets.cpp
View file

@ -93,7 +93,8 @@ static expr parse_structure_instance_core(parser & p, optional<expr> const & src
}
/* Parse rest of the qualified structure instance prefix '{' S '.' ... */
static expr parse_qualified_structure_instance(parser & p, name const & S) {
static expr parse_qualified_structure_instance(parser & p, name S, pos_info const & S_pos) {
S = p.to_constant(S, "invalid structure name", S_pos);
if (p.curr_is_token(get_rcurly_tk())) {
p.next();
buffer<name> fns;
@ -154,7 +155,7 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
}
} else if (p.curr_is_token(get_period_tk())) {
p.next();
return parse_qualified_structure_instance(p, id);
return parse_qualified_structure_instance(p, id, id_pos);
} else if (p.curr_is_token(get_assign_tk()) || p.curr_is_token(get_fieldarrow_tk())) {
return parse_structure_instance(p, id);
} else if (p.curr_is_token(get_membership_tk()) || p.curr_is_token(get_in_tk())) {

14
tests/lean/run/1703.lean Normal file
View file

@ -0,0 +1,14 @@
namespace ns
structure struct :=
(index : ℕ)
end ns
open ns
def foo : struct :=
{ ns.struct . index := 1 }
def foo2 : struct :=
{ struct . index := 1 }