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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Aesop.ElabM.runForwardElab goal x = Aesop.ElabM.run { parsePriorities := true, goal := goal } x

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

Equations

• Aesop.Frontend.mkForwardOptions maxDepth? traceScript = { traceScript := traceScript }.toOptions' maxDepth?

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

Equations

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

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

Equations

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

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

Equations

• Aesop.Frontend.mkHypForwardRule fvarId = do let __do_lift ← liftM (Lean.PrettyPrinter.delab (Lean.Expr.fvar fvarId)) Aesop.Frontend.elabForwardRule __do_lift

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

Equations

• Aesop.Frontend.isImplication e = Lean.Meta.forallBoundedTelescope e (some 1) fun (args : Array Lean.Expr) (body : Lean.Expr) => pure !args.isEmpty <&&> Lean.Meta.isProp body

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.Frontend.evalSaturateCore (stx : Lean.Syntax) (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

Equations

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

def Aesop.Frontend.saturate : Lean.ParserDescr

Equations

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

def Aesop.Frontend.saturate? : Lean.ParserDescr

Equations

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

def Aesop.Frontend.evalSaturate : Lean.Elab.Tactic.Tactic

Equations

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

def Aesop.Frontend.evalSaturate? : Lean.Elab.Tactic.Tactic

Equations

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

def Aesop.Frontend.tacticForward____ : Lean.ParserDescr

Equations

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

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

Equations

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