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

fix(inductive_cmd): intro rule names must be atomic identifiers

Browse source
This commit is contained in:
Daniel Selsam 2016-10-11 18:10:45 -07:00 • committed by Leonardo de Moura
parent 047556528d
commit 8d94dfd8e8
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/inductive_cmds.cpp
View file

@ -256,7 +256,7 @@ class inductive_cmd_fn {
m_p.next();
while (true) {
m_pos = m_p.pos();
name ir_name = mlocal_name(ind) + m_p.check_decl_id_next("invalid introduction rule, identifier expected");
name ir_name = mlocal_name(ind) + m_p.check_atomic_id_next("invalid introduction rule, atomic identifier expected");
if (prepend_ns)
ir_name = get_namespace(m_env) + ir_name;
m_implicit_infer_map.insert(ir_name, parse_implicit_infer_modifier(m_p));