Function expr_size_within 

pub fn expr_size_within(e: &Expr, cap: usize) -> bool

Check whether an expression has at most cap AST nodes (counted as a tree: a shared subterm counts once per occurrence).

Used to keep giant intermediate terms out of the whnf / def-eq caches: retaining every multi-million-node reduction step is what turned Lean core’s Int.add_mul_ediv_right into a multi-GiB peak (Init corpus, C16). Skipping cache retention for oversized terms never changes any verdict — only memoisation.

The answer is usually read off the term’s cached rebuild cost, in O(1). That cost (Expr::rebuild_cost) counts every node of the tree once and every leaf once more, so size <= cost <= 2 * size:

• cost <= cap — the size is within the cap (unless the cost is the saturated value, which only says “at least this much”);
• cost > 2 * cap — the size is over it. (The cost is stored saturated at REBUILD_COST_MAX; a saturated cost only understates the true one, so this bound still holds.)

Only a term whose cost falls between the two is counted, by a walk that visits at most cap + 1 nodes. Every def-eq step and every whnf result asks this question of its terms, and counting each of them was a tenth of the run time of a Mathlib replay once hashing no longer walked them.