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

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

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)