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✝¹)

Equations

• Lean.Elab.Tactic.Do.instDecidableEqFuel.decEq (Lean.Elab.Tactic.Do.Fuel.limited a) (Lean.Elab.Tactic.Do.Fuel.limited b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lean.Elab.Tactic.Do.instDecidableEqFuel.decEq (Lean.Elab.Tactic.Do.Fuel.limited n) Lean.Elab.Tactic.Do.Fuel.unlimited = isFalse ⋯
• Lean.Elab.Tactic.Do.instDecidableEqFuel.decEq Lean.Elab.Tactic.Do.Fuel.unlimited (Lean.Elab.Tactic.Do.Fuel.limited n) = isFalse ⋯
• Lean.Elab.Tactic.Do.instDecidableEqFuel.decEq Lean.Elab.Tactic.Do.Fuel.unlimited Lean.Elab.Tactic.Do.Fuel.unlimited = isTrue ⋯

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

Equations

• Lean.Elab.Tactic.Do.instDecidableEqFuel = Lean.Elab.Tactic.Do.instDecidableEqFuel.decEq

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

Equations

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

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.emitVC subGoal name = do let m ← liftM (Lean.Meta.mkFreshExprSyntheticOpaqueMVar subGoal name) Lean.Elab.Tactic.Do.addSubGoalAsVC m.mvarId! pure m

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.withJP {α : Type} (jp : FVarId) (info : JumpSiteInfo) : VCGenM α → VCGenM α

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.knownJP? jp = do let __do_lift ← read pure (Std.TreeMap.get? __do_lift.jps jp)

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.withLetDeclShared {α : Type} (name : Name) (type val : Expr) (k : Bool → 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.isJP (n : Name) : Bool

TODO: Fix this when rewriting the do elaborator

Equations

• Lean.Elab.Tactic.Do.isJP n = (n.eraseMacroScopes == `__do_jp)

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.

Equations

• Lean.Elab.Tactic.Do.reduceProjBeta? e = Lean.Elab.Tactic.Do.reduceProjBeta?.go✝ none e.getAppFn e.getAppRevArgs

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

Equations

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