structure Aesop.RuleFilter : Type

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

  #[] means 'match any builder'

• phases : Array Aesop.PhaseName

  #[] means 'match any phase'

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

Equations

• f.matchesPhase p = (f.phases.isEmpty || f.phases.contains p)

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

Equations

• f.matchesBuilder b = (f.builders.isEmpty || f.builders.contains b)

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

Equations

• f.matches n = (f.name == n.name && f.scope == n.scope && f.matchesPhase n.phase && f.matchesBuilder n.builder)

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

Equations

• f.matchesSimpTheorem? = if (f.scope == Aesop.ScopeName.global && f.matchesBuilder Aesop.BuilderName.simp) = true then some f.name else none

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

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

Equations

• One or more equations did not get rendered due to their size.

structure Aesop.RuleSetNameFilter : Type

• ns : Array Aesop.RuleSetName

def Aesop.RuleSetNameFilter.all : Aesop.RuleSetNameFilter

Equations

• Aesop.RuleSetNameFilter.all = { ns := #[] }

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

Equations

• f.matchesAll = f.ns.isEmpty

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

Equations

• f.matches n = (f.matchesAll || f.ns.contains n)

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

Equations

• f.matchedRuleSetNames = if f.matchesAll = true then none else some f.ns