WPApp: metadata for a goal whose right-hand side is a wp application, with isWPApp? to recognize one.

structure Lean.Elab.Tactic.Do.Internal.VCGen.WPApp : Type

Common metadata for a goal whose right-hand side is a weakest-precondition application pre ⊑ wp Prog Value Pred EPred instAL instEAL instWP prog post epost s₁ ... sₙ.

• head : Expr

  The wp function head, separated from its explicit core arguments.

• args : Array Expr

  The ordered core arguments of the wp application: #[Prog, Value, Pred, EPred, instAL, instEAL, instWP, prog, post, epost].

• excessArgs : Array Expr

  Extra arguments applied after wp … prog post epost, usually concrete state arguments.

def Lean.Elab.Tactic.Do.Internal.VCGen.WPApp.Prog (info : WPApp) : Expr

Program type argument of wp (e.g. m α or a non-monadic program type).

def Lean.Elab.Tactic.Do.Internal.VCGen.WPApp.M (info : WPApp) : Expr

The monad of an m α-shaped program type, obtained by dropping the value type α. For a non-monadic program type the type itself is returned.

def Lean.Elab.Tactic.Do.Internal.VCGen.WPApp.Value (info : WPApp) : Expr

Result/value type argument of wp.

def Lean.Elab.Tactic.Do.Internal.VCGen.WPApp.Pred (info : WPApp) : Expr

Predicate/lattice type argument of wp.

def Lean.Elab.Tactic.Do.Internal.VCGen.WPApp.EPred (info : WPApp) : Expr

Exception postcondition type argument of wp.

def Lean.Elab.Tactic.Do.Internal.VCGen.WPApp.instWP (info : WPApp) : Expr

WP instance argument of wp.

def Lean.Elab.Tactic.Do.Internal.VCGen.WPApp.prog (info : WPApp) : Expr

Program expression classified by VCGen.

def Lean.Elab.Tactic.Do.Internal.VCGen.WPApp.post (info : WPApp) : Expr

Postcondition argument of wp.

def Lean.Elab.Tactic.Do.Internal.VCGen.isWPApp? (rhs : Expr) : Option WPApp

The wp metadata of rhs, or none when rhs is not a wp application.