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

Equations

• Lean.Elab.Tactic.Do.instDecidableEqFuel = Lean.Elab.Tactic.Do.decEqFuel✝

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.VCGenM = ReaderT Lean.Elab.Tactic.Do.Context (StateRefT' IO.RealWorld Lean.Elab.Tactic.Do.State Lean.MetaM)

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.ifOutOfFuel x k = do let s ← get match s.fuel with | Lean.Elab.Tactic.Do.Fuel.limited 0 => x | x => k

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.addSubGoalAsVC goal = modify fun (s : Lean.Elab.Tactic.Do.State) => { fuel := s.fuel, simpState := s.simpState, vcs := s.vcs.push goal }

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.instMonadLiftSimpMVCGenM = { monadLift := fun {α : Type} (x : Lean.Meta.SimpM α) => Lean.Elab.Tactic.Do.liftSimpM x }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.bvar deBruijnIndex) = true
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.mvar mvarId) = true
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.fvar fvarId) = true
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.const declName us) = true
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.lit a) = true
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.sort u) = true
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.mdata data e_2) = Lean.Elab.Tactic.Do.isDuplicable e_2
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.proj typeName idx e_2) = Lean.Elab.Tactic.Do.isDuplicable e_2
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.lam binderName binderType body binderInfo) = false
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.forallE binderName binderType body binderInfo) = false
• Lean.Elab.Tactic.Do.isDuplicable (Lean.Expr.letE declName type value body nondep) = false
• Lean.Elab.Tactic.Do.isDuplicable (fn.app arg) = (fn.app arg).isAppOf `OfNat.ofNat

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.step.onFail goal name = Lean.Elab.Tactic.Do.emitVC goal.toExpr name

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)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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