source
structure Lean.Elab.Tactic.Do.VCGen.Result :
Type

- invariants : Array MVarId
- vcs : Array MVarId

Instances For

source
def Lean.Elab.Tactic.Do.VCGen.genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) :
MetaM Result
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) :
TacticM Unit
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.elabVCs (stx : Syntax) (vcs : Array MVarId) :
TacticM (List MVarId)
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.elabMVCGen :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.elabMVCGenHint :
Tactic
Equations

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

Instances For