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

fix: bug at ll_infer_type

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-04 13:55:06 -07:00
parent 7668750cb5
commit ffc90f6a35
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/ll_infer_type.cpp
View file

@ -62,6 +62,10 @@ class ll_infer_type_fn {
expr infer_cases(expr const & e) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() == 1) {
// This can happen for empty types. That is, the only argument is the major premise.
return mk_enf_object_type();
}
lean_assert(args.size() >= 2);
bool first = true;
expr r = *g_bot;