def Lean.Parser.Category.Hammer.solverOption : Category

Equations

• Lean.Parser.Category.Hammer.solverOption = { }

def Hammer.solverOption.quot : Lean.ParserDescr

Equations

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

def Hammer.preprocessing.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.Hammer.preprocessing : Category

Equations

• Lean.Parser.Category.Hammer.preprocessing = { }

def Lean.Parser.Category.Hammer.configOption : Category

Equations

• Lean.Parser.Category.Hammer.configOption = { }

def Hammer.configOption.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.Hammer.bool_lit : Category

Equations

• Lean.Parser.Category.Hammer.bool_lit = { }

def Hammer.bool_lit.quot : Lean.ParserDescr

Equations

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

def bool_litTrue : Lean.ParserDescr

Equations

• bool_litTrue = Lean.ParserDescr.node `bool_litTrue 1024 (Lean.ParserDescr.nonReservedSymbol "true" false)

def bool_litFalse : Lean.ParserDescr

Equations

• bool_litFalse = Lean.ParserDescr.node `bool_litFalse 1024 (Lean.ParserDescr.nonReservedSymbol "false" false)

opaque hammer.solverDefault : Lean.Option String

opaque hammer.solverTimeoutDefault : Lean.Option Nat

opaque hammer.preprocessingDefault : Lean.Option String

opaque hammer.disableAesopDefault : Lean.Option Bool

opaque hammer.disableAutoDefault : Lean.Option Bool

opaque hammer.autoPremisesDefault : Lean.Option Nat

opaque hammer.aesopPremisesDefault : Lean.Option Nat

opaque hammer.aesopPremisePriorityDefault : Lean.Option Nat

opaque hammer.aesopAutoPriorityDefault : Lean.Option Nat

def HammerCore.getHammerSolverDefault (opts : Lean.Options) : String

Equations

• HammerCore.getHammerSolverDefault opts = Lean.Option.get opts hammer.solverDefault

def HammerCore.getHammerSolverTimeoutDefault (opts : Lean.Options) : Nat

Equations

• HammerCore.getHammerSolverTimeoutDefault opts = Lean.Option.get opts hammer.solverTimeoutDefault

def HammerCore.getPreprocessingDefault (opts : Lean.Options) : String

Equations

• HammerCore.getPreprocessingDefault opts = Lean.Option.get opts hammer.preprocessingDefault

def HammerCore.getDisableAesopDefault (opts : Lean.Options) : Bool

Equations

• HammerCore.getDisableAesopDefault opts = Lean.Option.get opts hammer.disableAesopDefault

def HammerCore.getDisableAutoDefault (opts : Lean.Options) : Bool

Equations

• HammerCore.getDisableAutoDefault opts = Lean.Option.get opts hammer.disableAutoDefault

def HammerCore.getAutoPremisesDefault (opts : Lean.Options) : Nat

Equations

• HammerCore.getAutoPremisesDefault opts = Lean.Option.get opts hammer.autoPremisesDefault

def HammerCore.getAesopPremisesDefault (opts : Lean.Options) : Nat

Equations

• HammerCore.getAesopPremisesDefault opts = Lean.Option.get opts hammer.aesopPremisesDefault

def HammerCore.getAesopPremisePriorityDefault (opts : Lean.Options) : Nat

Equations

• HammerCore.getAesopPremisePriorityDefault opts = Lean.Option.get opts hammer.aesopPremisePriorityDefault

def HammerCore.getAesopAutoPriorityDefault (opts : Lean.Options) : Nat

Equations

• HammerCore.getAesopAutoPriorityDefault opts = Lean.Option.get opts hammer.aesopAutoPriorityDefault

def HammerCore.getHammerSolverDefaultM : Lean.CoreM String

Equations

• HammerCore.getHammerSolverDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getHammerSolverDefault opts)

def HammerCore.getHammerSolverTimeoutDefaultM : Lean.CoreM Nat

Equations

• HammerCore.getHammerSolverTimeoutDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getHammerSolverTimeoutDefault opts)

def HammerCore.getPreprocessingDefaultM : Lean.CoreM String

Equations

• HammerCore.getPreprocessingDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getPreprocessingDefault opts)

def HammerCore.getDisableAesopDefaultM : Lean.CoreM Bool

Equations

• HammerCore.getDisableAesopDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getDisableAesopDefault opts)

def HammerCore.getDisableAutoDefaultM : Lean.CoreM Bool

Equations

• HammerCore.getDisableAutoDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getDisableAutoDefault opts)

def HammerCore.getAutoPremisesDefaultM : Lean.CoreM Nat

Equations

• HammerCore.getAutoPremisesDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getAutoPremisesDefault opts)

def HammerCore.getAesopPremisesDefaultM : Lean.CoreM Nat

Equations

• HammerCore.getAesopPremisesDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getAesopPremisesDefault opts)

def HammerCore.getAesopPremisePriorityDefaultM : Lean.CoreM Nat

Equations

• HammerCore.getAesopPremisePriorityDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getAesopPremisePriorityDefault opts)

def HammerCore.getAesopAutoPriorityDefaultM : Lean.CoreM Nat

Equations

• HammerCore.getAesopAutoPriorityDefaultM = do let opts ← Lean.getOptions pure (HammerCore.getAesopAutoPriorityDefault opts)

def HammerCore.solverOptionZipperposition_exe : Lean.ParserDescr

Equations

• HammerCore.solverOptionZipperposition_exe = Lean.ParserDescr.node `HammerCore.solverOptionZipperposition_exe 1024 (Lean.ParserDescr.nonReservedSymbol "zipperposition_exe" false)

def HammerCore.solverOptionZipperposition : Lean.ParserDescr

Equations

• HammerCore.solverOptionZipperposition = Lean.ParserDescr.node `HammerCore.solverOptionZipperposition 1024 (Lean.ParserDescr.nonReservedSymbol "zipperposition" false)

def HammerCore.solverOptionCvc5 : Lean.ParserDescr

Equations

• HammerCore.solverOptionCvc5 = Lean.ParserDescr.node `HammerCore.solverOptionCvc5 1024 (Lean.ParserDescr.nonReservedSymbol "cvc5" false)

def HammerCore.preprocessingSimp_target : Lean.ParserDescr

Equations

• HammerCore.preprocessingSimp_target = Lean.ParserDescr.node `HammerCore.preprocessingSimp_target 1024 (Lean.ParserDescr.nonReservedSymbol "simp_target" false)

def HammerCore.preprocessingSimp_all : Lean.ParserDescr

Equations

• HammerCore.preprocessingSimp_all = Lean.ParserDescr.node `HammerCore.preprocessingSimp_all 1024 (Lean.ParserDescr.nonReservedSymbol "simp_all" false)

def HammerCore.preprocessingNo_preprocessing : Lean.ParserDescr

Equations

• HammerCore.preprocessingNo_preprocessing = Lean.ParserDescr.node `HammerCore.preprocessingNo_preprocessing 1024 (Lean.ParserDescr.nonReservedSymbol "no_preprocessing" false)

def HammerCore.preprocessingAesop : Lean.ParserDescr

Equations

• HammerCore.preprocessingAesop = Lean.ParserDescr.node `HammerCore.preprocessingAesop 1024 (Lean.ParserDescr.nonReservedSymbol "aesop" false)

inductive HammerCore.Solver : Type

• zipperposition_exe : Solver
• zipperposition : Solver
• cvc5 : Solver

instance HammerCore.instToExprSolver : Lean.ToExpr Solver

Equations

• HammerCore.instToExprSolver = { toExpr := HammerCore.toExprSolver✝, toTypeExpr := Lean.Expr.const `HammerCore.Solver [] }

instance HammerCore.instBEqSolver : BEq Solver

Equations

• HammerCore.instBEqSolver = { beq := HammerCore.beqSolver✝ }

inductive HammerCore.Preprocessing : Type

• simp_target : Preprocessing
• simp_all : Preprocessing
• no_preprocessing : Preprocessing
• aesop : Preprocessing

instance HammerCore.instBEqPreprocessing : BEq Preprocessing

Equations

• HammerCore.instBEqPreprocessing = { beq := HammerCore.beqPreprocessing✝ }

instance HammerCore.instToExprPreprocessing : Lean.ToExpr Preprocessing

Equations

• HammerCore.instToExprPreprocessing = { toExpr := HammerCore.toExprPreprocessing✝, toTypeExpr := Lean.Expr.const `HammerCore.Preprocessing [] }

def HammerCore.elabSolverOption {m : Type → Type} [Monad m] [Lean.MonadError m] (stx : Lean.TSyntax `Hammer.solverOption) : m Solver

Equations

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

def HammerCore.elabSolverOptionDefault : Lean.CoreM Solver

Equations

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

def HammerCore.elabPreprocessing {m : Type → Type} [Monad m] [Lean.MonadError m] (stx : Lean.TSyntax `Hammer.preprocessing) : m Preprocessing

Equations

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

def HammerCore.elabPreprocessingDefault : Lean.CoreM Preprocessing

Equations

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

def HammerCore.elabBoolLit {m : Type → Type} [Monad m] [Lean.MonadError m] (stx : Lean.TSyntax `Hammer.bool_lit) : m Bool

Equations

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

def HammerCore.«configOptionSolver:=_» : Lean.ParserDescr

Equations

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

def HammerCore.«configOptionSolverTimeout:=_» : Lean.ParserDescr

Equations

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

def HammerCore.«configOptionPreprocessing:=_» : Lean.ParserDescr

Equations

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

def HammerCore.«configOptionDisableAuto:=_» : Lean.ParserDescr

Equations

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

def HammerCore.«configOptionDisableAesop:=_» : Lean.ParserDescr

Equations

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

def HammerCore.«configOptionAutoPremises:=_» : Lean.ParserDescr

Equations

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

def HammerCore.«configOptionAesopPremises:=_» : Lean.ParserDescr

Equations

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

def HammerCore.«configOptionAesopPremisePriority:=_» : Lean.ParserDescr

Equations

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

def HammerCore.«configOptionAesopAutoPriority:=_» : Lean.ParserDescr

Equations

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

structure HammerCore.ConfigurationOptions : Type

• solver : Solver
• solverTimeout : Nat
• preprocessing : Preprocessing
• disableAuto : Bool
• disableAesop : Bool
• aesopPremisePriority : Nat
• aesopAutoPriority : Nat
• autoPremises : Nat
• aesopPremises : Nat

instance HammerCore.instToExprConfigurationOptions : Lean.ToExpr ConfigurationOptions

Equations

• HammerCore.instToExprConfigurationOptions = { toExpr := HammerCore.toExprConfigurationOptions✝, toTypeExpr := Lean.Expr.const `HammerCore.ConfigurationOptions [] }

def HammerCore.hammerStar : Lean.ParserDescr

Equations

• HammerCore.hammerStar = Lean.ParserDescr.nodeWithAntiquot "hammerStar" `HammerCore.hammerStar (Lean.ParserDescr.symbol "*")

def HammerCore.hammerCore : Lean.ParserDescr

Equations

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

def HammerCore.validateConfigOptions (configOptions : ConfigurationOptions) : Lean.Elab.Tactic.TacticM ConfigurationOptions

Checks to ensure that the set of given configOptions is usable.

Equations

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

def HammerCore.parseConfigOptions (configOptionsStx : Lean.TSyntaxArray `Hammer.configOption) : Lean.Elab.Tactic.TacticM ConfigurationOptions

Equations

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

def HammerCore.withSolverOptions {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] [Lean.MonadWithOptions m] (configOptions : ConfigurationOptions) (x : m α) : m α

Equations

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

def HammerCore.withDuperOptions {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] [Lean.MonadWithOptions m] (x : m α) : m α

Equations

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