Documentation

Lean.Elab.Tactic.Do.Spec

source
def Lean.Elab.Tactic.Do.findSpec (database : SpecAttr.SpecTheorems) (wp : Expr) :
MetaM SpecAttr.SpecTheorem
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Tactic.Do.mSpec {n : Type → Type u_1} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] (goal : ProofMode.MGoal) (elabSpecAtWP : Expr → n SpecAttr.SpecTheorem) (goalTag : Name) :
    n Expr

    Returns the proof and the list of new unassigned MVars.

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