max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/constructions/no_confusion): do not include propositions

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-11 17:36:04 -08:00
parent 9c24b81cbf
commit 95c93e7211
1 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/library/constructions/no_confusion.cpp
View file

@ -94,20 +94,21 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
throw_corrupted(n);
buffer<expr> rtype_hyp;
// add equalities
// proof irrelevance version using heterogeneous equality
for (unsigned i = 0; i < minor1_args.size(); i++) {
expr lhs = minor1_args[i];
expr rhs = minor2_args[i];
expr lhs_type = mlocal_type(lhs);
expr rhs_type = mlocal_type(rhs);
level l = sort_level(tc.ensure_type(lhs_type));
expr h_type;
if (tc.is_def_eq(lhs_type, rhs_type)) {
h_type = mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs);
} else {
h_type = mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs);
if (!tc.is_prop(lhs_type)) {
expr rhs_type = mlocal_type(rhs);
level l = sort_level(tc.ensure_type(lhs_type));
expr h_type;
if (tc.is_def_eq(lhs_type, rhs_type)) {
h_type = mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs);
} else {
h_type = mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs);
}
rtype_hyp.push_back(mk_local(mk_fresh_name(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info()));
}
rtype_hyp.push_back(mk_local(mk_fresh_name(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info()));
}
inner_cases_on_args.push_back(Fun(minor2_args, mk_arrow(Pi(rtype_hyp, P), Pres)));
}