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

chore(library/compiler/lcnf): add comment

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-14 12:03:17 -07:00
parent 5ed05db261
commit eb2d8543f7
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -439,14 +439,16 @@ public:
type_checker tc(m_st, m_lctx);
expr type = tc.whnf(tc.infer(e));
if (is_sort(type)) {
// Types are not pre-processed
/* Types are not pre-processed */
return cache_result(e, e, shared);
} else if (tc.is_prop(type)) {
// We replace proofs using `lc_proof` constant
/* 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
/* Functions that return types are not pre-processed.
This is a partial (and quick) check since we are not using
`whnf` on nested terms. */
while (is_pi(type))
type = binding_body(type);
if (is_sort(type))