structure Lean.Elab.Tactic.VCGen.ExcessArgsFrameInfo : Type

The frames of a precondition pre for the excess state arguments s₁ … sₙ of a goal pre ⊑ X s₁ … sₙ. For n = 2, frames is #[fun u₁ => ⌜u₁ = s₁⌝ ⊓ fun u₂ => ⌜u₂ = s₂⌝ ⊓ pre, fun u₂ => ⌜u₂ = s₂⌝ ⊓ pre, pre]. Its first entry frame holds at s₁ s₂ exactly where pre holds, and is ⊥ at every other pair of states, so pre ⊑ X s₁ s₂ and frame ⊑ X are equivalent.

• frames : Array Expr

def Lean.Elab.Tactic.VCGen.ExcessArgsFrameInfo.new (pre : Expr) (ss : Array Expr) : MetaM ExcessArgsFrameInfo

Build the frames of pre for the excess state arguments ss.

Equations

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

def Lean.Elab.Tactic.VCGen.ExcessArgsFrameInfo.frame (i : ExcessArgsFrameInfo) : Expr

The frame of pre for all excess state arguments.

Equations

• i.frame = i.frames[0]!

def Lean.Elab.Tactic.VCGen.ExcessArgsFrameInfo.instantiate (i : ExcessArgsFrameInfo) (X : Expr) (ss : Array Expr) (h : Expr) : MetaM Expr

Turn h : frame ⊑ X into a proof of pre ⊑ X s₁ … sₙ.

Equations

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

def Lean.Elab.Tactic.VCGen.ExcessArgsFrameInfo.abstract (i : ExcessArgsFrameInfo) (X : Expr) (ss : Array Expr) (h : Expr) : MetaM Expr

Turn h : pre ⊑ X s₁ … sₙ into a proof of frame ⊑ X.

Equations

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