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