def Lean.Elab.Tactic.elabCalcSteps (steps : Array Lean.Syntax) : Lean.Elab.Tactic.TacticM Lean.Expr

Equations

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

def Lean.Elab.Tactic.elabCalcSteps.go (steps : Array Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Equations

• Lean.Elab.Tactic.elabCalcSteps.go steps = do let e ← Lean.Elab.Term.elabCalcSteps steps Lean.Elab.Term.synthesizeSyntheticMVars false false Lean.instantiateMVars e

def Lean.Elab.Tactic.evalCalc : Lean.Elab.Tactic.Tactic

Elaborator for the calc tactic mode variant.

Equations

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