structure Aesop.Rule (α : Type) : Type

• name : Aesop.RuleName
• indexingMode : Aesop.IndexingMode
• extra : α
• tac : Aesop.RuleTacDescr

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

Equations

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

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

Equations

• Aesop.Rule.instBEqRule = { beq := fun r s => r.name == s.name }

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

Equations

• Aesop.Rule.instOrdRule = { compare := fun r s => compare r.name s.name }

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

Equations

• Aesop.Rule.instHashableRule = { hash := fun r => hash r.name }

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

Equations

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

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

Equations

• Aesop.Rule.compareByName r s = Aesop.RuleName.compare r.name s.name

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

Equations

• Aesop.Rule.compareByPriorityThenName r s = match Aesop.Rule.compareByPriority r s with | Ordering.eq => Aesop.Rule.compareByName r s | ord => ord

@[inline]

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

Equations

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

@[inline]

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

Equations

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