← Mathematical handbook

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

Equations

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

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

Equations

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

def Aesop.RuleFilter.matches (f : RuleFilter) (n : 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 : 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 : RuleFilter) : Option Lean.Name

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

Equations

• f.matchesLocalNormSimpRule? = (if (f.scope == Aesop.ScopeName.local && f.matchesBuilder Aesop.BuilderName.simp) = true then pure (some f.name) else pure none).run

structure Aesop.RuleSetNameFilter : Type

• ns : Array RuleSetName

def Aesop.RuleSetNameFilter.all : RuleSetNameFilter

Equations

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

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

Equations

• f.matchesAll = f.ns.isEmpty

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

Equations

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

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

Equations

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