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✝)

Equations

• Aesop.instInhabitedRule = { default := Aesop.instInhabitedRule.default }

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

Equations

• Aesop.instInhabitedRule.default = { name := default, indexingMode := default, pattern? := default, extra := default, tac := default }

@[implicit_reducible]

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

Equations

• Aesop.Rule.instBEq = { beq := fun (r s : Aesop.Rule α) => r.name == s.name }

@[implicit_reducible]

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

Equations

• Aesop.Rule.instOrd = { compare := fun (r s : Aesop.Rule α) => compare r.name s.name }

@[implicit_reducible]

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

Equations

• Aesop.Rule.instHashable = { hash := fun (r : Aesop.Rule α) => hash r.name }

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

Equations

• r.compareByPriority s = compare r.extra s.extra

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

Equations

• r.compareByName s = r.name.compare s.name

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

Equations

• r.compareByPriorityThenName s = (r.compareByPriority s).then (r.compareByName s)

@[inline]

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

Equations

• Aesop.Rule.map f r = { name := r.name, indexingMode := r.indexingMode, pattern? := r.pattern?, extra := f r.extra, tac := r.tac }

@[inline]

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

Equations

• Aesop.Rule.mapM f r = do let __do_lift ← f r.extra pure { name := r.name, indexingMode := r.indexingMode, pattern? := r.pattern?, extra := __do_lift, tac := r.tac }