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

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

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

def Lean.Elab.Tactic.Do.instDecidableEqFuel.decEq (x✝ x✝¹ : Fuel) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

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

def Lean.Elab.Tactic.Do.elabConfig (cfg : Syntax) (init : VCGen.Config := { }) (logExceptions : Bool := true) : TacticM VCGen.Config

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

• numJoinParams : Nat

  Number of join point arguments.

• altIdx : Nat

  Index of the match alternative.

• altParams : Array Expr

  Parameter FVars of the match alternative.

• altLCtxIdx : Nat

  The size of the local context in the alternative after the match has been split and all splitter parameters have been introduced. This is so that we can construct the Σ Lᵢ part of the hyps field.

• hyps : MVarId

  MVar to be filled with the stateful hypotheses of the match arm. This should include bindings from the local context Lᵢ of the call site and is of the form (x,y,z ∈ Lᵢ) Σ Lᵢ, ⌜x = a ∧ y = b ∧ z = c⌝ ∧ Hᵢ, where ..., Lᵢ ⊢ Hᵢ ⊢ₛ wp[jp x y z] Q is the call site. The Σ Lᵢ is short for something like let x := ...; ∃ y (h : y = ...), ∃ z, ∃ (h₂ : p).

• joinPrf : Expr

  The proof that jump sites should use to discharge Hᵢ ⊢ₛ wp[jp a b c] Q.

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

• config : VCGen.Config
• specThms : SpecAttr.SpecTheorems
• simpCtx : Meta.Simp.Context
• simprocs : Meta.Simp.SimprocsArray
• jps : FVarIdMap JumpSiteInfo
• initialCtxSize : Nat

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

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

  Holes of type Invariant that have been generated so far.

• vcs : Array MVarId

  The verification conditions that have been generated so far.

@[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.addSubGoalAsVC (goal : MVarId) : VCGenM PUnit

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

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

@[implicit_reducible]

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

def Lean.Elab.Tactic.Do.withJP {α : Type} (jp : FVarId) (info : JumpSiteInfo) : VCGenM α → VCGenM α

def Lean.Elab.Tactic.Do.knownJP? (jp : FVarId) : VCGenM (Option JumpSiteInfo)

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

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

def Lean.Elab.Tactic.Do.isJP (n : Name) : Bool

TODO: Fix this when rewriting the do elaborator

partial def Lean.Elab.Tactic.Do.getNumJoinParams (joinTy resTy : Expr) : MetaM Nat

def Lean.Elab.Tactic.Do.reduceProjBeta? (e : Expr) : MetaM (Option Expr)

Reduces (1) Prod projection functions and (2) Projs in application heads, and (3) beta reduces. Will not unfold projection functions unless further beta reduction happens.

def Lean.Elab.Tactic.Do.mkSpecContext (optConfig lemmas : Syntax) (ignoreStarArg : Bool := false) : TacticM Context

def Lean.Elab.Tactic.Do.withLocalSpecs {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT VCGenM m] (xs : Array Expr) (k : m α) : m α