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

fix(kernel/inductive): bug in inductive datatype computational rule, we *must* first instantiate universe variables, *and then* the arguments

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-30 14:15:16 -07:00
parent 6e6f778ecf
commit e3f9b21c30
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/standard/logic.lean
View file

@ -85,8 +85,7 @@ theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀
definition cast {A B : Type} (H : A = B) (a : A) : B definition cast {A B : Type} (H : A = B) (a : A) : B
:= eq_rec a H := eq_rec a H
-- TODO(Leo): check why unifier needs 'help' in the following theorem theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a
theorem cast_refl.{l} {A : Type.{l}} (a : A) : cast (refl A) a = a
:= refl (cast (refl A) a) := refl (cast (refl A) a)
definition iff (a b : Bool) := (a → b) ∧ (b → a) definition iff (a b : Bool) := (a → b) ∧ (b → a)

4
src/kernel/inductive/inductive.cpp
View file

@ -798,8 +798,8 @@ optional<expr> inductive_normalizer_extension::operator()(expr const & e, extens
for (unsigned i = 0; i < it2->m_num_bu; i++) for (unsigned i = 0; i < it2->m_num_bu; i++)
ACebu.push_back(intro_args[it1->m_num_params + i]); ACebu.push_back(intro_args[it1->m_num_params + i]);
std::reverse(ACebu.begin(), ACebu.end()); std::reverse(ACebu.begin(), ACebu.end());
expr r = instantiate(it2->m_comp_rhs_body, ACebu.size(), ACebu.data()); expr r = instantiate_univ_params(it2->m_comp_rhs_body, it1->m_level_names, const_levels(elim_fn));
r = instantiate_univ_params(r, it1->m_level_names, const_levels(elim_fn)); r = instantiate(r, ACebu.size(), ACebu.data());
return some_expr(r); return some_expr(r);
} }