opaque Lean.Elab.Tactic.Do.mvcgen.warning : Lean.Option Bool

inductive Lean.Elab.Tactic.Do.Fuel : Type

• limited (n : Nat) : Fuel
• unlimited : Fuel

instance Lean.Elab.Tactic.Do.instDecidableEqFuel : DecidableEq Fuel

structure Lean.Elab.Tactic.Do.Config : Type

• noLetElim : Bool

  If true, do not substitute away let-declarations that are used at most once before starting VC generation.

def Lean.Elab.Tactic.Do.elabConfig : Syntax → TacticM Config

structure Lean.Elab.Tactic.Do.Context : Type

• config : Config
• specThms : SpecAttr.SpecTheorems
• simpCtx : Meta.Simp.Context
• simprocs : Meta.Simp.SimprocsArray

structure Lean.Elab.Tactic.Do.State : Type

• fuel : Fuel
• simpState : Meta.Simp.State
• vcs : Array MVarId

  The verification conditions that have been generated so far. Includes Type-valued goals arising from instantiation of specifications.

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.VCGenM (α : Type) : Type

def Lean.Elab.Tactic.Do.burnOne : VCGenM PUnit

def Lean.Elab.Tactic.Do.ifOutOfFuel {α : Type} (x k : VCGenM α) : VCGenM α

def Lean.Elab.Tactic.Do.emitVC (subGoal : Expr) (name : Name) : VCGenM Expr

def Lean.Elab.Tactic.Do.addSubGoalAsVC (goal : MVarId) : VCGenM PUnit

def Lean.Elab.Tactic.Do.liftSimpM {α : Type} (x : Meta.SimpM α) : VCGenM α

instance Lean.Elab.Tactic.Do.instMonadLiftSimpMVCGenM : MonadLift Meta.SimpM VCGenM

def Lean.Elab.Tactic.Do.mvcgen_step : ParserDescr

def Lean.Elab.Tactic.Do.mvcgen_no_trivial : ParserDescr

def Lean.Elab.Tactic.Do.mvcgen : ParserDescr

def Lean.Elab.Tactic.Do.isDuplicable (e : Expr) : Bool

def Lean.Elab.Tactic.Do.withSharing {α : Type} (name : Name) (type val : Expr) (k : Expr → (Expr → VCGenM Expr) → VCGenM α) (kind : LocalDeclKind := LocalDeclKind.default) : VCGenM α

def Lean.Elab.Tactic.Do.step (ctx : Context) (fuel : Fuel) (goal : ProofMode.MGoal) (name : Name) : MetaM (Expr × Array MVarId)

def Lean.Elab.Tactic.Do.step.onFail (goal : ProofMode.MGoal) (name : Name) : VCGenM Expr

partial def Lean.Elab.Tactic.Do.step.tryGoal (ctx : Context) (goal : Expr) (name : Name) : VCGenM Expr

partial def Lean.Elab.Tactic.Do.step.assignMVars (ctx : Context) (mvars : List MVarId) : VCGenM PUnit

partial def Lean.Elab.Tactic.Do.step.onGoal (ctx : Context) (goal : ProofMode.MGoal) (name : Name) : VCGenM Expr

partial def Lean.Elab.Tactic.Do.step.onImp (ctx : Context) (goal : ProofMode.MGoal) (name : Name) : VCGenM Expr

partial def Lean.Elab.Tactic.Do.step.onLambda (ctx : Context) (goal : ProofMode.MGoal) (name : Name) : VCGenM Expr

partial def Lean.Elab.Tactic.Do.step.onWPApp (ctx : Context) (goal : ProofMode.MGoal) (name : Name) : VCGenM Expr

def Lean.Elab.Tactic.Do.genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : TacticM (Array MVarId)

def Lean.Elab.Tactic.Do.elabMVCGenStep : Tactic

def Lean.Elab.Tactic.Do.elabMVCGenNoTrivial : Tactic

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