def Lean.Elab.Tactic.elabNativeDecideCore (tacticName : Name) (expectedType : Expr) : TacticM Expr

Equations

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

def Lean.Elab.Tactic.evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit

Equations

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

def Lean.Elab.Tactic.elabDecideConfig (cfg : Syntax) (init : Parser.Tactic.DecideConfig := { }) (logExceptions : Bool := true) : TacticM Parser.Tactic.DecideConfig

Equations

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

def Lean.Elab.Tactic.evalDecide : Tactic

Equations

• Lean.Elab.Tactic.evalDecide stx = do let cfg ← Lean.Elab.Tactic.elabDecideConfig stx[1] Lean.Elab.Tactic.evalDecideCore `decide cfg

def Lean.Elab.Tactic.evalNativeDecide : Tactic

Equations

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