def HammerCore.removeHammerStar (facts : Lean.Syntax.TSepArray [`HammerCore.hammerStar, `term] ",") : Bool × Lean.Syntax.TSepArray `term ","

Given a Syntax.TSepArray of facts provided by the user (which may include * to indicate that hammer should read in the full local context) removeHammerStar returns the Syntax.TSepArray with * removed and a boolean that indicates whether * was included in the original input.

Equations

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

def HammerCore.duperNativeSolverFunc (lemmas _inhLemmas : Array Auto.Lemma) : Lean.MetaM Lean.Expr

Equations

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

def HammerCore.throwSimpPreprocessingError {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (e : Lean.Exception) : m α

Equations

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

def HammerCore.throwTranslationError {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (e : Lean.Exception) : m α

Equations

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

def HammerCore.throwExternalSolverError {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (e : Lean.Exception) : m α

Equations

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

def HammerCore.throwDuperError {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (e : Lean.Exception) : m α

Equations

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

def HammerCore.throwProofFitError {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (e : Lean.Exception) : m α

Equations

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

def HammerCore.errorIsSimpPreprocessingError (e : Lean.Exception) : IO Bool

A function to determine whether an error thrown by hammer was generated by throwSimpPreprocessingError

Equations

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

def HammerCore.errorIsTranslationError (e : Lean.Exception) : IO Bool

A function to determine whether an error thrown by hammer was generated by throwTranslationError

Equations

• HammerCore.errorIsTranslationError e = do let eStr ← liftM e.toMessageData.toString pure ("hammer failed to preprocess facts for translation.".isPrefixOf eStr)

def HammerCore.errorIsExternalSolverError (e : Lean.Exception) : IO Bool

A function to determine whether an error thrown by hammer was generated by throwExternalSolverError

Equations

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

def HammerCore.errorIsDuperSolverError (e : Lean.Exception) : IO Bool

A function to determine whether an error thrown by hammer was generated by throwDuperError

Equations

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

def HammerCore.errorIsProofFitError (e : Lean.Exception) : IO Bool

A function to determine whether an error thrown by hammer was generated by throwProofFitError

Equations

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

def HammerCore.runHammerCore (stxRef : Lean.Syntax) (simpLemmas : Lean.Syntax.TSepArray [`Lean.Parser.Tactic.simpErase, `Lean.Parser.Tactic.simpLemma] ",") (premises : Lean.Syntax.TSepArray `term ",") (includeLCtx : Bool) (configOptions : ConfigurationOptions) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def HammerCore.evalHammerCore : Lean.Elab.Tactic.Tactic

Equations

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