From a5b9a7b2965d295c06f92c3b8a2b528cfb2248db Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jul 2014 11:10:45 -0700 Subject: [PATCH] fix(frontends/lean/decl_cmds): support for section declarations with implicit parameters, they must be tagged with '@' when creating aliases Signed-off-by: Leonardo de Moura --- library/standard/diaconescu.lean | 2 +- src/frontends/lean/decl_cmds.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/library/standard/diaconescu.lean b/library/standard/diaconescu.lean index cb39fa754e..730693fb6a 100644 --- a/library/standard/diaconescu.lean +++ b/library/standard/diaconescu.lean @@ -8,7 +8,7 @@ using eq_proofs -- Show that Excluded middle follows from -- Hilbert's choice operator, function extensionality and Prop extensionality section -hypothesis propext ⦃a b : Prop⦄ : (a → b) → (b → a) → a = b +hypothesis propext {a b : Prop} : (a → b) → (b → a) → a = b parameter p : Prop diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index b7a6e711d9..28ee51e916 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -258,6 +258,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { type = Pi_as_is(section_ps, type, p); value = Fun_as_is(section_ps, value, p); levels section_ls = collect_section_levels(ls, p); + for (expr & p : section_ps) + p = mk_explicit(p); expr ref = mk_implicit(mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps)); p.add_local_expr(n, ref); }