def Aesop.Frontend.Parser.usingRuleSets : Lean.ParserDescr

def Aesop.Frontend.Parser.additionalRule : Lean.ParserDescr

def Aesop.Frontend.Parser.additionalRules : Lean.ParserDescr

def Aesop.ElabM.runForwardElab {α : Type} (goal : Lean.MVarId) (x : ElabM α) : Lean.Elab.TermElabM α

def Aesop.Frontend.mkForwardOptions (maxDepth? : Option Nat) (traceScript : Bool) : Lean.CoreM Options'

def Aesop.Frontend.elabGlobalRuleSets (rsNames : Array Lean.Ident) : Lean.CoreM (Array (GlobalRuleSet × Lean.Name × Lean.Name))

def Aesop.Frontend.elabForwardRule (term : Lean.Term) : ElabM LocalRuleSetMember

def Aesop.Frontend.mkHypForwardRule (fvarId : Lean.FVarId) : ElabM LocalRuleSetMember

def Aesop.Frontend.isImplication (e : Lean.Expr) : Lean.MetaM Bool

def Aesop.Frontend.mkHypImplicationRule? (fvarId : Lean.FVarId) : ElabM (Option LocalRuleSetMember)

def Aesop.Frontend.addLocalImplications (rs : LocalRuleSet) : ElabM LocalRuleSet

def Aesop.Frontend.elabAdditionalForwardRules (rs : LocalRuleSet) (rules : Array (Lean.TSyntax `Aesop.Frontend.Parser.additionalRule)) : ElabM LocalRuleSet

def Aesop.Frontend.elabForwardRuleSetCore (rsNames : Array Lean.Ident) (additionalRules : Array (Lean.TSyntax `Aesop.Frontend.Parser.additionalRule)) (options : Options') : ElabM LocalRuleSet

def Aesop.Frontend.elabForwardRuleSet (rsNames? : Option (Lean.TSyntax `Aesop.Frontend.Parser.usingRuleSets)) (additionalRules? : Option (Lean.TSyntax `Aesop.Frontend.Parser.additionalRules)) (options : Options') : ElabM LocalRuleSet

def Aesop.Frontend.evalSaturate (depth? : Option (Lean.TSyntax `num)) (rules? : Option (Lean.TSyntax `Aesop.Frontend.Parser.additionalRules)) (rs? : Option (Lean.TSyntax `Aesop.Frontend.Parser.usingRuleSets)) (traceScript : Bool) : Lean.Elab.Tactic.TacticM Unit

def Aesop.Frontend.tacticSaturate_____ : Lean.ParserDescr

def Aesop.Frontend.tacticSaturate?_____ : Lean.ParserDescr

def Aesop.Frontend.tacticForward___ : Lean.ParserDescr

def Aesop.Frontend.tacticForward?___ : Lean.ParserDescr