From eb2d8543f7883b8d742ef50183fcd8c8046ea4dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Sep 2018 12:03:17 -0700 Subject: [PATCH] chore(library/compiler/lcnf): add comment --- src/library/compiler/lcnf.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index 2e0d27bc24..fdde045c93 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -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))