Documentation

Lean.Elab.Tactic.Do.VCGen

source
structure Lean.Elab.Tactic.Do.VCGen.Result :
Type
Instances For
    source
    def Lean.Elab.Tactic.Do.VCGen.genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) :
    MetaM Result
    Equations
      Instances For
        source
        def Lean.Elab.Tactic.Do.elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) :
        TacticM Unit
        Equations
          Instances For
            source
            def Lean.Elab.Tactic.Do.elabVCs (stx : Syntax) (vcs : Array MVarId) :
            TacticM (List MVarId)
            Equations
              Instances For
                source
                def Lean.Elab.Tactic.Do.elabMVCGen :
                Tactic
                Equations
                  Instances For
                    source
                    def Lean.Elab.Tactic.Do.elabMVCGenHint :
                    Tactic
                    Equations
                      Instances For