def Aesop.matchByTactic? : Lean.Term → Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def Aesop.RuleBuilder.tacticIMode (imode? : Option IndexingMode) : IndexingMode

Equations

• Aesop.RuleBuilder.tacticIMode imode? = imode?.getD Aesop.IndexingMode.unindexed

def Aesop.RuleBuilder.tacticCore (t : Lean.Name ⊕ Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (imode? : Option IndexingMode) (phase : PhaseSpec) : Lean.MetaM LocalRuleSetMember

Equations

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

def Aesop.RuleBuilder.tactic : RuleBuilder

Equations

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