structure Aesop.RuleFilter : Type

• name : Lean.Name
• scope : ScopeName
• builders : Array BuilderName

  #[] means 'match any builder'

• phases : Array PhaseName

  #[] means 'match any phase'

def Aesop.RuleFilter.matchesPhase (f : RuleFilter) (p : PhaseName) : Bool

def Aesop.RuleFilter.matchesBuilder (f : RuleFilter) (b : BuilderName) : Bool

def Aesop.RuleFilter.matches (f : RuleFilter) (n : RuleName) : Bool

def Aesop.RuleFilter.matchesSimpTheorem? (f : RuleFilter) : Option Lean.Name

def Aesop.RuleFilter.matchesLocalNormSimpRule? (f : RuleFilter) : Option Lean.Name

Returns the identifier of the local norm simp rule matched by f, if any.

structure Aesop.RuleSetNameFilter : Type

• ns : Array RuleSetName

def Aesop.RuleSetNameFilter.all : RuleSetNameFilter

def Aesop.RuleSetNameFilter.matchesAll (f : RuleSetNameFilter) : Bool

def Aesop.RuleSetNameFilter.matches (f : RuleSetNameFilter) (n : RuleSetName) : Bool

def Aesop.RuleSetNameFilter.matchedRuleSetNames (f : RuleSetNameFilter) : Option (Array RuleSetName)