structure Aesop.Rule (α : Type) : Type

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[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, pattern? := r.pattern?, 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, pattern? := r.pattern?, extra := __do_lift, tac := r.tac }