opaque Lean.Meta.Tactic.Cbv.cbv.warning : Lean.Option Bool

def Lean.Meta.Tactic.Cbv.cbvEntry (e : Expr) : MetaM Sym.Simp.Result

Equations

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

def Lean.Meta.Tactic.Cbv.cbvGoalCore (m : MVarId) (inv : Bool := false) : MetaM (Option MVarId)

Equations

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

def Lean.Meta.Tactic.Cbv.cbvGoal (m : MVarId) : MetaM (Option MVarId)

Equations

• Lean.Meta.Tactic.Cbv.cbvGoal m = do let __do_lift ← Lean.Meta.Tactic.Cbv.cbvGoalCore m match __do_lift with | none => pure none | some m' => Lean.Meta.Tactic.Cbv.cbvGoalCore m' true