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

fix(library/compiler/lcnf): it was not erasing proofs that start with Pi

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-12 18:26:23 -07:00
parent 379c06faf4
commit 7f496f43f1
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/lcnf.cpp
View file

@ -464,16 +464,16 @@ public:
if (is_sort(type)) {
// Types are not pre-processed
return cache_result(e, e, shared);
} else if (tc.is_prop(type)) {
// We replace proofs using `lc_proof` constant
expr r = mk_app(mk_constant(get_lc_proof_name()), type);
return cache_result(e, r, shared);
} else if (is_pi(type)) {
// Functions that return types are not pre-processed
while (is_pi(type))
type = binding_body(type);
if (is_sort(type))
return cache_result(e, e, shared);
} else if (tc.is_prop(type)) {
// We replace proofs using `lc_proof` constant
expr r = mk_app(mk_constant(get_lc_proof_name()), type);
return cache_result(e, r, shared);
}
}