Documentation
Aesop
.
RuleSet
.
Name
Search
return to top
source
Imports
Init
Lean
Imported by
Aesop
.
RuleSetName
Aesop
.
defaultRuleSetName
Aesop
.
builtinRuleSetName
Aesop
.
localRuleSetName
Aesop
.
builtinRuleSetNames
Aesop
.
RuleSetName
.
isReserved
source
@[reducible, inline]
abbrev
Aesop
.
RuleSetName
:
Type
Equations
Aesop.RuleSetName
=
Lean.Name
Instances For
source
def
Aesop
.
defaultRuleSetName
:
RuleSetName
Equations
Aesop.defaultRuleSetName
=
`default
Instances For
source
def
Aesop
.
builtinRuleSetName
:
RuleSetName
Equations
Aesop.builtinRuleSetName
=
`builtin
Instances For
source
def
Aesop
.
localRuleSetName
:
RuleSetName
Equations
Aesop.localRuleSetName
=
`local
Instances For
source
def
Aesop
.
builtinRuleSetNames
:
Array
RuleSetName
Equations
Aesop.builtinRuleSetNames
=
#[
Aesop.defaultRuleSetName
,
Aesop.builtinRuleSetName
]
Instances For
source
def
Aesop
.
RuleSetName
.
isReserved
(n :
RuleSetName
)
:
Bool
Equations
n
.
isReserved
=
(
n
==
Aesop.localRuleSetName
||
Aesop.builtinRuleSetNames
.
contains
n
)
Instances For