Documentation

Hammer.Tactic

source
def Hammer.hammer :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Hammer.runHammer (stxRef : Lean.Syntax) (simpLemmas : Lean.Syntax.TSepArray [`Lean.Parser.Tactic.simpErase, `Lean.Parser.Tactic.simpLemma] ",") (userInputTerms premises : Array Lean.Term) (includeLCtx : Bool) (configOptions : HammerCore.ConfigurationOptions) :
    Lean.Elab.Tactic.TacticM Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Hammer.evalHammer :
      Lean.Elab.Tactic.Tactic
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For