source
structure Aesop.Rule (α : Type) :
Type

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

Instances For

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

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

Instances For

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

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

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

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

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

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

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

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

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

- r.compareByPriority s = compare r.extra s.extra

Instances For

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

- r.compareByName s = r.name.compare s.name

Instances For

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

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

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For