Ceil simplifier - #4157

Draft

ehildenb wants to merge 4 commits into

ceil-simplifier

Commits on Jun 18, 2026

Pattern/Util: add collectUndefinedSubterms

ehildenb
and
claude
committed
2989081
Pattern/ApplyEquations: add evaluateCeils mode for runtime definedness discharge

ehildenb
and
claude
committed
8759dfa
booster/Pattern/Implies: switch MatchIndeterminate LHS-simplify to evaluatePatternWithCeils

ehildenb
and
claude
committed
673ad29
Pattern/Implies: simplify consequent under antecedent constraints

ehildenb
and
claude
committed
7ca9fd6