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.

def Lean.Meta.Tactic.Cbv.mkAppNS (f : Expr) (args : Array Expr) : Sym.SymM Expr

Equations

• Lean.Meta.Tactic.Cbv.mkAppNS f args = Array.foldlM Lean.Meta.Sym.Internal.mkAppS f args

def Lean.Meta.Tactic.Cbv.isVal (e : Expr) : Bool

Equations

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

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.

Equations

• Lean.Meta.Tactic.Cbv.isBuiltinValue e = pure (Lean.Meta.Sym.Simp.Result.rfl (Lean.Meta.Tactic.Cbv.isVal e))

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

Equations

• Lean.Meta.Tactic.Cbv.guardSimproc p s e = if p e = true then s e else pure Lean.Meta.Sym.Simp.Result.rfl

def Lean.Meta.Tactic.Cbv.isProofTerm : Sym.Simp.Simproc

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

Equations

• Lean.Meta.Tactic.Cbv.isProofTerm e = do let __do_lift ← liftM (Lean.Meta.Tactic.Cbv.isProof✝ e) pure (Lean.Meta.Sym.Simp.Result.rfl __do_lift)