Documentation

Aesop.Rule.Basic

structure Aesop.Rule (α : Type) :

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

Instances For

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 α) :

Equations

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

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

Equations

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

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

Equations

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

@[inline]

def Aesop.Rule.map {α : Type} {β : Type} (f : α → β) (r : 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 }