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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Tactic.Do.elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) :
      TacticM Unit
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.Tactic.Do.elabVCs (stx : Syntax) (vcs : Array MVarId) :
        TacticM (List MVarId)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.Tactic.Do.elabMVCGen :
          Tactic
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Elab.Tactic.Do.elabMVCGenHint :
            Tactic
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For