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
    Instances For
      source
      def Lean.Elab.Tactic.Do.elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) :
      TacticM Unit
      Instances For
        source
        def Lean.Elab.Tactic.Do.elabVCs (stx : Syntax) (vcs : Array MVarId) :
        TacticM (List MVarId)
        Instances For
          source
          def Lean.Elab.Tactic.Do.elabMVCGen :
          Tactic
          Instances For
            source
            def Lean.Elab.Tactic.Do.elabMVCGenHint :
            Tactic
            Instances For