From a2e36e97f220660fb954f745da24232deb200450 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Sep 2014 12:13:29 -0700 Subject: [PATCH] fix(frontends/lean/builtin_cmds): allow coercion command inside section, fixes #186 --- src/frontends/lean/builtin_cmds.cpp | 14 ++++---------- tests/lean/run/coesec.lean | 9 +++++++++ 2 files changed, 13 insertions(+), 10 deletions(-) create mode 100644 tests/lean/run/coesec.lean diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 6612fece9..10dd0debe 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -295,19 +295,13 @@ environment open_cmd(parser & p) { return open_export_cmd(p, true); } environment export_cmd(parser & p) { return open_export_cmd(p, false); } environment coercion_cmd(parser & p) { - auto pos = p.pos(); - expr f = p.parse_expr(); - if (!is_constant(f)) - throw parser_error("invalid 'coercion' command, constant expected", pos); + name f = p.check_constant_next("invalid 'coercion' command, constant expected"); if (p.curr_is_token(g_colon)) { p.next(); - pos = p.pos(); - expr C = p.parse_expr(); - if (!is_constant(C)) - throw parser_error("invalid 'coercion' command, constant expected", pos); - return add_coercion(p.env(), const_name(f), const_name(C), p.ios()); + name C = p.check_constant_next("invalid 'coercion' command, constant expected"); + return add_coercion(p.env(), f, C, p.ios()); } else { - return add_coercion(p.env(), const_name(f), p.ios()); + return add_coercion(p.env(), f, p.ios()); } } diff --git a/tests/lean/run/coesec.lean b/tests/lean/run/coesec.lean new file mode 100644 index 000000000..d4c428d55 --- /dev/null +++ b/tests/lean/run/coesec.lean @@ -0,0 +1,9 @@ +inductive func (A B : Type) := +mk : (A → B) → func A B + +section + parameters {A B : Type} + definition to_function (F : func A B) : A → B := + func.rec (λf, f) F + coercion to_function +end