structure Aesop.Rule (α : Type) : Type

• name : RuleName
• indexingMode : IndexingMode
• pattern? : Option RulePattern
• extra : α
• tac : RuleTacDescr

@[implicit_reducible]

instance Aesop.instInhabitedRule {a✝ : Type} [Inhabited a✝] : Inhabited (Rule a✝)

def Aesop.instInhabitedRule.default {a✝ : Type} [Inhabited a✝] : Rule a✝

@[implicit_reducible]

instance Aesop.Rule.instBEq {α : Type} : BEq (Rule α)

@[implicit_reducible]

instance Aesop.Rule.instOrd {α : Type} : Ord (Rule α)

@[implicit_reducible]

instance Aesop.Rule.instHashable {α : Type} : Hashable (Rule α)

def Aesop.Rule.compareByPriority {α : Type} [Ord α] (r s : Rule α) : Ordering

def Aesop.Rule.compareByName {α : Type} (r s : Rule α) : Ordering

def Aesop.Rule.compareByPriorityThenName {α : Type} [Ord α] (r s : Rule α) : Ordering

@[inline]

def Aesop.Rule.map {α β : Type} (f : α → β) (r : Rule α) : Rule β

@[inline]

def Aesop.Rule.mapM {m : Type → Type u_1} {α β : Type} [Monad m] (f : α → m β) (r : Rule α) : m (Rule β)