Ground Term Evaluation for Sym.dsimp

This module provides simplification procedures (Simproc) for evaluating ground terms of builtin types. It is designed for the Sym.dsimp simplifier and addresses performance issues in the standard Meta.Simp simprocs.

def Lean.Meta.Sym.DSimp.commandDeclare_eval_bin__ : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Sym.DSimp.commandDeclare_eval_bin_bitwise__ : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Sym.DSimp.commandDeclare_eval_bin_bool_pred__ : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Meta.Sym.DSimp.EvalStepConfig : Type

• maxExponent : Nat

def Lean.Meta.Sym.DSimp.evalGround (config : EvalStepConfig := { }) : DSimproc

Simplification procedure that evaluates ground terms of builtin types.

Important: This procedure assumes subterms have already been simplified. It evaluates a single operation on literal arguments only. For example:

• 2 + 3 → evaluates to 5
• 2 + (3 * 4) → returns .rfl (the argument 3 * 4 is not a literal)

The simplifier is responsible for term traversal, ensuring subterms are reduced before evalGround is called on the parent expression.

Equations

• One or more equations did not get rendered due to their size.