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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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