Diagnostic Utilities for Interval Tactics

Error reporting, shadow diagnostics, and helpful error messages for interval tactics.

def LeanCert.Tactic.Auto.extractIntervalBoundsForDiag (intervalInfo : IntervalInfo) : Option (ℚ × ℚ)

Extract interval bounds as rationals for diagnostics

Equations

• LeanCert.Tactic.Auto.extractIntervalBoundsForDiag intervalInfo = match intervalInfo.fromSetIcc with | some (lo, hi, fst, fst_1, fst_2, fst_3, snd) => some (lo, hi) | none => none

def LeanCert.Tactic.Auto.formatGoalContext (goalType : Lean.Expr) : Lean.MetaM Lean.MessageData

Format context of the goal for diagnostics

Equations

• LeanCert.Tactic.Auto.formatGoalContext goalType = pure (Lean.toMessageData "Goal: " ++ Lean.toMessageData goalType)

partial def LeanCert.Tactic.Auto.countForallsAux (e : Lean.Expr) (acc : ℕ) : Lean.MetaM ℕ

Count foralls in an expression

partial def LeanCert.Tactic.Auto.findComparisonAux (e : Lean.Expr) : Lean.MetaM (Option String)

Try to find the comparison in the body

def LeanCert.Tactic.Auto.analyzeGoalStructure (goalType : Lean.Expr) : Lean.MetaM Lean.MessageData

Analyze goal structure for diagnostics

Equations

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

def LeanCert.Tactic.Auto.suggestNextActions (tacticName : String) (goalType : Lean.Expr) : Lean.MetaM Lean.MessageData

Suggest next actions based on analysis

Equations

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

def LeanCert.Tactic.Auto.mkDiagnosticReport (tacticName : String) (goalType : Lean.Expr) (stage : String) (hint : Option Lean.MessageData := none) : Lean.MetaM Lean.MessageData

Generate a diagnostic report for parse errors

Equations

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