Documentation

Lean.Meta.Tactic.Cbv.Util

Cbv Utility Functions #

Predicates for recognizing ground literal values (isVal, isBuiltinValue) and proof terms (isProofTerm) in the SymM monad. Both are used by cbvPre to short-circuit before structural dispatch.

source
def Lean.Meta.Tactic.Cbv.mkAppNS (f : Expr) (args : Array Expr) :
Sym.SymM Expr
Instances For
    source
    def Lean.Meta.Tactic.Cbv.isVal (e : Expr) :
    Bool
    Instances For
      source
      def Lean.Meta.Tactic.Cbv.isBuiltinValue :
      Sym.Simp.Simproc

      Returns .rfl (done := true) for ground literal values of any recognized builtin type, preventing the simplifier from recursing into them. For example, this stops the evaluator from trying to unfold OfNat.ofNat 2 further.

      Instances For
        source
        def Lean.Meta.Tactic.Cbv.guardSimproc (p : Expr → Bool) (s : Sym.Simp.Simproc) :
        Sym.Simp.Simproc
        Instances For
          source
          def Lean.Meta.Tactic.Cbv.isProofTerm :
          Sym.Simp.Simproc

          Marks proof terms as done so the simplifier does not recurse into them.

          Instances For