Accessible names from the program

A specification theorem introduces binders, such as the a of a lambda fun a => e. vcgen introduces a inaccessibly as a✝, because tactic.hygienic is set.

A specification can state where an accessible name comes from. It states such a lambda as fun a => binderNameHint a (fun acc => p) e, where fun acc => p is a subexpression of the program. vcgen then introduces a accessibly as acc. This module implements that step. binderNameHint v binder e is the identity on e, so the specification states the same assertion.

Spec.bind states the hint over the continuation f:

Triple (x >>= f) (wp x (fun a => binderNameHint a f (wp (f a) post epost)) epost) post epost

For a program let acc ← e, the continuation f is fun acc => p. vcgen renames the variable it introduced for a to acc, so the verification condition states acc rather than a✝.

def Lean.Elab.Tactic.VCGen.consumeBinderNameHint? (goal : MVarId) (target : Expr) : VCGenM (Option MVarId)

Consume the hints of the target, and of either side of pre ⊑ rhs. A hint of the precondition is consumed before the precondition becomes a hypothesis.

Equations

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