From e3f9b21c301717dc92a073636282bf7a0089fb41 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Jun 2014 14:15:16 -0700 Subject: [PATCH] fix(kernel/inductive): bug in inductive datatype computational rule, we *must* first instantiate universe variables, *and then* the arguments Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 3 +-- src/kernel/inductive/inductive.cpp | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index 9f9dfcdf7c..bc1aa98d63 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -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 := eq_rec a H --- TODO(Leo): check why unifier needs 'help' in the following theorem -theorem cast_refl.{l} {A : Type.{l}} (a : A) : cast (refl A) a = a +theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a := refl (cast (refl A) a) definition iff (a b : Bool) := (a → b) ∧ (b → a) diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 9917660700..c1c2ba2255 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -798,8 +798,8 @@ optional inductive_normalizer_extension::operator()(expr const & e, extens for (unsigned i = 0; i < it2->m_num_bu; i++) ACebu.push_back(intro_args[it1->m_num_params + i]); std::reverse(ACebu.begin(), ACebu.end()); - expr r = instantiate(it2->m_comp_rhs_body, ACebu.size(), ACebu.data()); - r = instantiate_univ_params(r, it1->m_level_names, const_levels(elim_fn)); + expr r = instantiate_univ_params(it2->m_comp_rhs_body, it1->m_level_names, const_levels(elim_fn)); + r = instantiate(r, ACebu.size(), ACebu.data()); return some_expr(r); }