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

fix(frontends/lean/decl_cmds): support for section declarations with implicit parameters, they must be tagged with '@' when creating aliases

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-25 11:10:45 -07:00
parent 811f46e97b
commit a5b9a7b296
2 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/standard/diaconescu.lean
View file

@ -8,7 +8,7 @@ using eq_proofs
-- Show that Excluded middle follows from -- Show that Excluded middle follows from
-- Hilbert's choice operator, function extensionality and Prop extensionality -- Hilbert's choice operator, function extensionality and Prop extensionality
section 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 parameter p : Prop

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

@ -258,6 +258,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
type = Pi_as_is(section_ps, type, p); type = Pi_as_is(section_ps, type, p);
value = Fun_as_is(section_ps, value, p); value = Fun_as_is(section_ps, value, p);
levels section_ls = collect_section_levels(ls, 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)); expr ref = mk_implicit(mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps));
p.add_local_expr(n, ref); p.add_local_expr(n, ref);
} }