source
structure Aesop.RuleFilter :
Type

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

  `#[]` means 'match any builder'

- phases : Array PhaseName

  `#[]` means 'match any phase'

Instances For

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

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

Instances For

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

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

Instances For

source
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)

Instances For

source
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

Instances For

source
def Aesop.RuleFilter.matchesLocalNormSimpRule? (f : 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.

Instances For

source
structure Aesop.RuleSetNameFilter :
Type

- ns : Array RuleSetName

Instances For

source
def Aesop.RuleSetNameFilter.all :
RuleSetNameFilter
Equations

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

Instances For

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

- f.matchesAll = f.ns.isEmpty

Instances For

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

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

Instances For

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

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

Instances For