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

fix(frontends/lean/inductive_cmd): bugs when declarating inductive datatypes in sections, fixes #141, fixes #142

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-05 19:02:18 -07:00
parent e4a687c5ea
commit b5f595c432
2 changed files with 31 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/inductive_cmd.cpp
View file

@ -379,7 +379,7 @@ struct inductive_cmd_fn {
[&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); }))
return none_expr();
// found target
expr r = mk_app(mk_explicit(e), section_params);
expr r = mk_implicit(mk_app(mk_explicit(e), section_params));
return some_expr(r);
});
}
@ -512,15 +512,16 @@ struct inductive_cmd_fn {
}
/** \brief Create an alias for the fully qualified name \c full_id. */
environment create_alias(environment env, bool composite, name const & full_id, levels const & section_leves, buffer<expr> const & section_params) {
environment create_alias(environment env, bool composite, name const & full_id, levels const & section_levels, buffer<expr> const & section_params) {
name id;
if (composite)
id = name(name(full_id.get_prefix().get_string()), full_id.get_string());
else
id = name(full_id.get_string());
if (in_section_or_context(env)) {
expr r = mk_explicit(mk_constant(full_id, section_leves));
expr r = mk_explicit(mk_constant(full_id, section_levels));
r = mk_app(r, section_params);
r = mk_implicit(r);
m_p.add_local_expr(id, r);
}
if (full_id != id)

27
tests/lean/run/class_bug1.lean Normal file
View file

@ -0,0 +1,27 @@
import logic
inductive category (ob : Type) (mor : ob → ob → Type) : Type :=
mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
(id : Π {A : ob}, mor A A),
(Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
comp h (comp g f) = comp (comp h g) f) →
(Π {A B : ob} {f : mor A B}, comp f id = f) →
(Π {A B : ob} {f : mor A B}, comp id f = f) →
category ob mor
class category
namespace category
section sec_cat
parameter A : Type
inductive foo :=
mk : A → foo
class foo
parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
abbreviation compose := rec (λ comp id assoc idr idl, comp) Cat
abbreviation id := rec (λ comp id assoc idr idl, id) Cat
infixr `∘`:60 := compose
inductive is_section {A B : ob} (f : mor A B) : Type :=
mk : ∀g, g ∘ f = id → is_section f
end sec_cat
end category