def Lean.Elab.Tactic.Cbv.cbvLocalDecl (fvarId : FVarId) : TacticM Unit

Reduces the type of hypothesis fvarId using cbv, in its own SymM session.

def Lean.Elab.Tactic.Cbv.cbvTarget : TacticM Unit

Reduces the goal target using cbv, in its own SymM session.

def Lean.Elab.Tactic.Cbv.evalCbv : Tactic

def Lean.Elab.Tactic.Cbv.evalDecideCbv : Tactic