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

fix(frontends/lean/structure_cmd): error parsing structure without parameters followed by ': Type'

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-05 11:43:39 -08:00
parent defc2478b5
commit d6dc624ca8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -108,7 +108,7 @@ struct structure_cmd_fn {
/** \brief Parse structure parameters */
void parse_params() {
if (!m_p.curr_is_token(get_extends_tk()) && !m_p.curr_is_token(get_assign_tk()))
if (!m_p.curr_is_token(get_extends_tk()) && !m_p.curr_is_token(get_assign_tk()) && !m_p.curr_is_token(get_colon_tk()))
m_p.parse_binders(m_params);
for (expr const & l : m_params)
m_p.add_local(l);