Skip to content

Commit

Permalink
chore: document change
Browse files Browse the repository at this point in the history
  • Loading branch information
leodemoura committed Aug 6, 2024
1 parent 3439180 commit 8f6ba0e
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions src/kernel/expr_eq_fn.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,10 @@ class expr_eq_fn {
return false;
}
void check_system(unsigned depth) {
/*
We used to use `lean::check_system` here. We claim it is ok to not check memory consumption here.
Note that `do_check_interrupted` was set to `false`. Thus, `check_interrupted` and `check_heartbeat` were not being used.
*/
if (depth > m_max_stack_depth) {
if (m_max_stack_depth > 0)
throw stack_space_exception("expression equality test");
Expand Down

0 comments on commit 8f6ba0e

Please sign in to comment.