From bf13b24692ce5b96cb8a9fd4a3d11c0e170dbccf Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 23 Nov 2024 18:13:51 +0100 Subject: [PATCH] doc: refine kernel code comments (#6150) I just spent too much time being confused about the kernel type checker until I noticed that `lazy_delta_reduction` modifies its arguments. --- src/kernel/type_checker.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 012ae00de9..b0e6844dca 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -981,6 +981,7 @@ lbool type_checker::is_def_eq_offset(expr const & t, expr const & s) { return l_undef; } +/** \remark t_n, s_n are updated. */ lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) { while (true) { lbool r = is_def_eq_offset(t_n, s_n); @@ -1098,6 +1099,7 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) { r = is_def_eq_proof_irrel(t_n, s_n); if (r != l_undef) return r == l_true; + /* NB: `lazy_delta_reduction` updates `t_n` and `s_n` even when returning `l_undef`. */ r = lazy_delta_reduction(t_n, s_n); if (r != l_undef) return r == l_true;