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.instBEqRule {α : Type} : BEq (Aesop.Rule α)

Equations

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

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

Equations

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

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

Equations

• Aesop.Rule.instHashableRule = { hash := fun (r : Aesop.Rule α) => 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 = Ordering.then (Aesop.Rule.compareByPriority r s) (Aesop.Rule.compareByName r 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 }