inductive EvalAuto.Result : Type

• success : Result
• nonProp : Result
• typeCheckFail : Result
• typeUnequal : Result
• nonterminate : Result
• subGoals : Result
• exception (e : Lean.Exception) : Result

instance EvalAuto.instInhabitedResult : Inhabited Result

Equations

• EvalAuto.instInhabitedResult = { default := EvalAuto.Result.success }

instance EvalAuto.instToMessageDataResult : Lean.ToMessageData Result

Equations

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

def EvalAuto.Result.concise : Result → String

Equations

• EvalAuto.Result.success.concise = "S"
• EvalAuto.Result.nonProp.concise = "N"
• EvalAuto.Result.typeCheckFail.concise = "F"
• EvalAuto.Result.typeUnequal.concise = "U"
• EvalAuto.Result.nonterminate.concise = "T"
• EvalAuto.Result.subGoals.concise = "G"
• (EvalAuto.Result.exception e).concise = "E"

def EvalAuto.Result.ofConcise? : String → Option Result

Equations

• One or more equations did not get rendered due to their size.
• EvalAuto.Result.ofConcise? "S" = some EvalAuto.Result.success
• EvalAuto.Result.ofConcise? "N" = some EvalAuto.Result.nonProp
• EvalAuto.Result.ofConcise? "F" = some EvalAuto.Result.typeCheckFail
• EvalAuto.Result.ofConcise? "U" = some EvalAuto.Result.typeUnequal
• EvalAuto.Result.ofConcise? "T" = some EvalAuto.Result.nonterminate
• EvalAuto.Result.ofConcise? "G" = some EvalAuto.Result.subGoals
• EvalAuto.Result.ofConcise? x✝ = none

def EvalAuto.Result.ofTacticOnExpr (e : Lean.Expr) (tactic : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.TermElabM Result

Run tactic on a metavariable with type e and obtain the result

Equations

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