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

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

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

Equations

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

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

Equations

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

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

Equations

• Aesop.RuleFilter.matchesSimpTheorem? f = if (f.scope == Aesop.ScopeName.global && Aesop.RuleFilter.matchesBuilder f 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

• Aesop.RuleSetNameFilter.matchesAll f = Array.isEmpty f.ns

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

Equations

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

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

Equations

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