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

structure Lean.Elab.Tactic.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ₙ.

• expr : Expr

  The whole wp application, including the excess state arguments.

• 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.VCGen.WPApp.Prog (info : WPApp) : Expr

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

Equations

• info.Prog = info.args[0]!

def Lean.Elab.Tactic.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.

Equations

• info.M = if info.args[0]!.isApp = true then info.args[0]!.appFn! else info.args[0]!

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

Result/value type argument of wp.

Equations

• info.Value = info.args[1]!

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

Predicate/lattice type argument of wp.

Equations

• info.Pred = info.args[2]!

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

Exception postcondition type argument of wp.

Equations

• info.EPred = info.args[3]!

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

WP instance argument of wp.

Equations

• info.instWP = info.args[6]!

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

Program expression classified by VCGen.

Equations

• info.prog = info.args[7]!

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

Postcondition argument of wp.

Equations

• info.post = info.args[8]!

def Lean.Elab.Tactic.VCGen.WPApp.wp (info : WPApp) : Expr

The wp application itself, before the excess state arguments apply.

Equations

• info.wp = info.expr.stripArgsN info.excessArgs.size

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

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

Equations

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