Documentation

Aesop.Rule.Basic

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} :
Equations
  • Aesop.Rule.instBEq = { beq := fun (r s : Aesop.Rule α) => r.name == s.name }
instance Aesop.Rule.instOrd {α : Type} :
Equations
Equations
  • Aesop.Rule.instHashable = { hash := fun (r : Aesop.Rule α) => hash r.name }
Equations
  • r.compareByPriority s = compare r.extra s.extra
Equations
  • r.compareByName s = r.name.compare s.name
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 : TypeType u_1} {α : Type} {β : Type} [Monad m] (f : αm β) (r : Aesop.Rule α) :
m (Aesop.Rule β)
Equations
  • Aesop.Rule.mapM f r = do let __do_liftf r.extra pure { name := r.name, indexingMode := r.indexingMode, pattern? := r.pattern?, extra := __do_lift, tac := r.tac }