From 8d94dfd8e8e6f20b41ec69edb0016e746b49d6db Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 11 Oct 2016 18:10:45 -0700 Subject: [PATCH] fix(inductive_cmd): intro rule names must be atomic identifiers --- src/frontends/lean/inductive_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 0831eaa299..1c09091396 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -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));