From f339f97975acc9bd699883953d102fc4e9ccd31f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Jun 2017 12:52:52 -0700 Subject: [PATCH] fix(frontends/lean/brackets): fixes #1703 --- src/frontends/lean/brackets.cpp | 5 +++-- tests/lean/run/1703.lean | 14 ++++++++++++++ 2 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/1703.lean diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp index 517ff87823..61b40d5e0e 100644 --- a/src/frontends/lean/brackets.cpp +++ b/src/frontends/lean/brackets.cpp @@ -93,7 +93,8 @@ static expr parse_structure_instance_core(parser & p, optional 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 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())) { diff --git a/tests/lean/run/1703.lean b/tests/lean/run/1703.lean new file mode 100644 index 0000000000..68c56b7d4c --- /dev/null +++ b/tests/lean/run/1703.lean @@ -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 }