Documentation

Aesop.Util.Tactic

A MetaM version of the replace tactic. If fvarId refers to the hypothesis h, this tactic asserts a new hypothesis h : type with proof proof : type and then tries to clear fvarId. Unlike replaceLocalDecl, replaceFVar always adds the new hypothesis at the end of the local context.

replaceFVar returns the new goal, the FVarId of the newly asserted hypothesis and whether the old hypothesis was cleared.

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

    Introduce as many binders as possible while unfolding definitions with the ambient transparency.

    Equations
    Instances For