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

fix(frontends/lean/elaborator): better specific universe detection

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-09 14:43:07 -07:00
parent 8f1b6178a7
commit 052bc6ff20
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/algebra/relation.lean
View file

@ -23,10 +23,10 @@ mk : reflexive R → is_reflexive R
namespace is_reflexive namespace is_reflexive
definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_reflexive R) : reflexive R := definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_reflexive R) : reflexive R :=
is_reflexive.rec (λu, u) C is_reflexive.rec (λu, u) C
definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_reflexive R} : reflexive R := definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_reflexive R} : reflexive R :=
is_reflexive.rec (λu, u) C is_reflexive.rec (λu, u) C
end is_reflexive end is_reflexive
@ -37,10 +37,10 @@ mk : symmetric R → is_symmetric R
namespace is_symmetric namespace is_symmetric
definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_symmetric R) : symmetric R := definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_symmetric R) : symmetric R :=
is_symmetric.rec (λu, u) C is_symmetric.rec (λu, u) C
definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_symmetric R} : symmetric R := definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_symmetric R} : symmetric R :=
is_symmetric.rec (λu, u) C is_symmetric.rec (λu, u) C
end is_symmetric end is_symmetric
@ -51,10 +51,10 @@ mk : transitive R → is_transitive R
namespace is_transitive namespace is_transitive
definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_transitive R) : transitive R := definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_transitive R) : transitive R :=
is_transitive.rec (λu, u) C is_transitive.rec (λu, u) C
definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_transitive R} : transitive R := definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_transitive R} : transitive R :=
is_transitive.rec (λu, u) C is_transitive.rec (λu, u) C
end is_transitive end is_transitive

4
src/frontends/lean/elaborator.cpp
View file

@ -1054,8 +1054,8 @@ std::tuple<expr, level_param_names> elaborator::operator()(list<expr> const & ct
auto p = solve(cs).pull(); auto p = solve(cs).pull();
lean_assert(p); lean_assert(p);
substitution s = p->first.first; substitution s = p->first.first;
check_sort_assignments(s);
auto result = apply(s, r); auto result = apply(s, r);
check_sort_assignments(s);
copy_info_to_manager(s); copy_info_to_manager(s);
return result; return result;
} }
@ -1081,11 +1081,11 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(
auto p = solve(cs).pull(); auto p = solve(cs).pull();
lean_assert(p); lean_assert(p);
substitution s = p->first.first; substitution s = p->first.first;
check_sort_assignments(s);
name_set univ_params = collect_univ_params(r_v, collect_univ_params(r_t)); name_set univ_params = collect_univ_params(r_v, collect_univ_params(r_t));
buffer<name> new_params; buffer<name> new_params;
expr new_r_t = apply(s, r_t, univ_params, new_params); expr new_r_t = apply(s, r_t, univ_params, new_params);
expr new_r_v = apply(s, r_v, univ_params, new_params); expr new_r_v = apply(s, r_v, univ_params, new_params);
check_sort_assignments(s);
copy_info_to_manager(s); copy_info_to_manager(s);
return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end())); return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end()));
} }