Intrinsic verification syntax

A definition carrying given xs / requires P / ensures b => Q 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 clauses into the plain def plus a spec theorem @[spec] theorem f.spec : ∀ xs, ⦃P⦄ f args ⦃fun b => Q⦄ 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.elabContractNotice : Command.CommandElab

Report the experimental status of each contract clause the notice carries.

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.