- regular (b : BuilderName) : DBuilderName
- default : DBuilderName
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
def
Aesop.Frontend.elabTransparency :
Lean.TSyntax `Aesop.Frontend.Parser.transparency → Lean.Elab.TermElabM Lean.Meta.TransparencyMode
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
- immediate (names : Array Lean.Name) : BuilderOption
- index (imode : IndexingMode) : BuilderOption
- pattern (stx : Lean.Term) : BuilderOption
- casesPatterns (pats : Array CasesPattern) : BuilderOption
- transparency (md : Lean.Meta.TransparencyMode) (alsoForIndex : Bool) : BuilderOption
Instances For
Equations
Instances For
Equations
Instances For
- builder? : Option DBuilderName
- builderOptions : RuleBuilderOptions
- ruleSets : RuleSets
Instances For
def
Aesop.Frontend.RuleConfig.addFeature
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
:
Feature → m RuleConfig
Equations
Instances For
def
Aesop.Frontend.RuleConfig.getPenalty
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(phase : PhaseName)
(c : RuleConfig)
:
m Int
Equations
Instances For
def
Aesop.Frontend.RuleConfig.getSuccessProbability
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
:
m Percent
Equations
Instances For
def
Aesop.Frontend.RuleConfig.getSimpPriority
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
:
m Nat
Equations
Instances For
def
Aesop.Frontend.RuleConfig.getTerm
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
:
Equations
Instances For
def
Aesop.Frontend.RuleConfig.getPhase
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
:
Equations
Instances For
def
Aesop.Frontend.RuleConfig.getBuilder
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
:
Equations
Instances For
def
Aesop.Frontend.RuleConfig.getPhaseSpec
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
:
Equations
Instances For
Equations
Instances For
Equations
Instances For
def
Aesop.Frontend.RuleConfig.validateForAdditionalRules
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
(defaultRuleSet : RuleSetName)
:
Equations
Instances For
def
Aesop.Frontend.RuleConfig.validateForAdditionalRules.getPhaseAndPriority
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(c : RuleConfig)
:
Equations
Instances For
def
Aesop.Frontend.RuleExpr.toRuleConfigs
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(e : RuleExpr)
(init : RuleConfig)
:
m (Array RuleConfig)
Equations
Instances For
def
Aesop.Frontend.RuleExpr.toAdditionalRules
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(e : RuleExpr)
(init : RuleConfig)
(defaultRuleSet : RuleSetName)
:
m (Array RuleConfig)
Equations
Instances For
def
Aesop.Frontend.RuleExpr.toAdditionalGlobalRules
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(decl? : Option Lean.Name)
(e : RuleExpr)
:
m (Array RuleConfig)