Documentation

Lean.Meta.Sym.DSimp.EvalGround

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.

source
def Lean.Meta.Sym.DSimp.commandDeclare_eval_bin__ :
ParserDescr
Instances For
    source
    def Lean.Meta.Sym.DSimp.commandDeclare_eval_bin_bitwise__ :
    ParserDescr
    Instances For
      source
      def Lean.Meta.Sym.DSimp.commandDeclare_eval_bin_bool_pred__ :
      ParserDescr
      Instances For
        source
        structure Lean.Meta.Sym.DSimp.EvalStepConfig :
        Type
        • maxExponent : Nat
        Instances For
          source
          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.

          Instances For