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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

source
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.

Instances For

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

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

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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
Equations

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

Instances For

source
def Aesop.Frontend.tacticSaturate_____ :
Lean.ParserDescr
Equations

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

Instances For

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

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

Instances For

source
def Aesop.Frontend.tacticForward___ :
Lean.ParserDescr
Equations

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

Instances For

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

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

Instances For