Intrinsic verification syntax

A definition carrying given xs / requires P / ensures b => Q / throws e => R clauses expands to the plain definition plus a vcgen-proven, @[spec]-tagged specification theorem f.spec. An assert element in a do block elaborates to the assertion gadget that vcgen proves in the course of that theorem.

def Lean.Elab.Tactic.Do.contractBinderIdents (binder : Syntax) : Array Ident

The identifiers bound by an explicit (…) binder, used to apply the definition in its spec.

Equations

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

def Lean.Elab.Tactic.Do.expandDefContract : Macro

Expand a def carrying given/requires/ensures/throws clauses into the plain def plus a spec theorem @[spec] theorem f.spec : ∀ xs, ⦃P⦄ f args ⦃fun b => Q; E⦄ proved by vcgen. A where finally | spec => steps section supplies grind-mode steps for the verification conditions finish leaves open.

Equations

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

def Lean.Elab.Tactic.Do.elabContractEPosts : Term.TermElab

Elaborating contract_eposts% e unfolds the EPostSlot.set applications and ⊥ in e, e.g. to an estack⟨...⟩ expression. Used in the expansion of throws clauses to yield simpler specs.

Equations

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

def Lean.Elab.Tactic.Do.elabContractNotice : Command.CommandElab

Report the experimental status of each contract clause the notice carries, in a slight command-level misuse of a contractDeclVal node. Does not change the environment.

Equations

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

def Lean.Elab.Tactic.Do.elabDoAssertion : Do.DoElab

Equations

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