Documentation

Lean.Elab.Tactic.Do.VCGen

  • noLetElim : Bool

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

Equations
  • One or more equations did not get rendered due to their size.
  • fuel : Fuel
  • simpState : Meta.Simp.State
  • The verification conditions that have been generated so far. Includes Type-valued goals arising from instantiation of specifications.

Equations
  • One or more equations did not get rendered due to their size.
Equations
def Lean.Elab.Tactic.Do.emitVC (subGoal : Expr) (name : Name) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.Do.withSharing {α : Type} (name : Name) (type val : Expr) (k : Expr(ExprVCGenM Expr)VCGenM α) (kind : LocalDeclKind := LocalDeclKind.default) :
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) :
Equations
  • One or more equations did not get rendered due to their size.
partial def Lean.Elab.Tactic.Do.step.tryGoal (ctx : Context) (goal : Expr) (name : Name) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.