Documentation
Lean
.
Data
.
NameMap
Search
Google site search
Lean
.
Data
.
NameMap
source
Imports
Init
Lean.Data.HashSet
Lean.Data.Name
Lean.Data.RBMap
Lean.Data.RBTree
Lean.Data.SSet
Imported by
Lean
.
instCoeStringName_1
Lean
.
NameMap
Lean
.
mkNameMap
Lean
.
NameMap
.
instEmptyCollectionNameMap
Lean
.
NameMap
.
instInhabitedNameMap
Lean
.
NameMap
.
insert
Lean
.
NameMap
.
contains
Lean
.
NameMap
.
find?
Lean
.
NameMap
.
instForInNameMapProdName
Lean
.
NameSet
Lean
.
NameSet
.
empty
Lean
.
NameSet
.
instEmptyCollectionNameSet
Lean
.
NameSet
.
instInhabitedNameSet
Lean
.
NameSet
.
insert
Lean
.
NameSet
.
contains
Lean
.
NameSet
.
instForInNameSetName
Lean
.
NameSSet
Lean
.
NameSSet
.
empty
Lean
.
NameSSet
.
instEmptyCollectionNameSSet
Lean
.
NameSSet
.
instInhabitedNameSSet
Lean
.
NameSSet
.
insert
Lean
.
NameSSet
.
contains
Lean
.
NameHashSet
Lean
.
NameHashSet
.
empty
Lean
.
NameHashSet
.
instEmptyCollectionNameHashSet
Lean
.
NameHashSet
.
instInhabitedNameHashSet
Lean
.
NameHashSet
.
insert
Lean
.
NameHashSet
.
contains
Lean
.
MacroScopesView
.
isPrefixOf
Lean
.
MacroScopesView
.
isSuffixOf
source
instance
Lean
.
instCoeStringName_1
:
Coe
String
Lake.Name
source
def
Lean
.
NameMap
(α :
Type
)
:
Type
Instances For
source
@[inline]
def
Lean
.
mkNameMap
(α :
Type
)
:
Lake.NameMap
α
Instances For
source
instance
Lean
.
NameMap
.
instEmptyCollectionNameMap
(α :
Type
)
:
EmptyCollection
(
Lake.NameMap
α
)
source
instance
Lean
.
NameMap
.
instInhabitedNameMap
(α :
Type
)
:
Inhabited
(
Lake.NameMap
α
)
source
def
Lean
.
NameMap
.
insert
{α :
Type
}
(m :
Lake.NameMap
α
)
(n :
Lake.Name
)
(a :
α
)
:
Lean.RBMap
Lake.Name
α
Lean.Name.quickCmp
Instances For
source
def
Lean
.
NameMap
.
contains
{α :
Type
}
(m :
Lake.NameMap
α
)
(n :
Lake.Name
)
:
Bool
Instances For
source
@[inline]
def
Lean
.
NameMap
.
find?
{α :
Type
}
(m :
Lake.NameMap
α
)
(n :
Lake.Name
)
:
Option
α
Instances For
source
instance
Lean
.
NameMap
.
instForInNameMapProdName
{α :
Type
}
{m :
Type
u_1 →
Type
u_2
}
:
ForIn
m
(
Lake.NameMap
α
) (
Lake.Name
×
α
)
source
def
Lean
.
NameSet
:
Type
Instances For
source
def
Lean
.
NameSet
.
empty
:
Lean.NameSet
Instances For
source
instance
Lean
.
NameSet
.
instEmptyCollectionNameSet
:
EmptyCollection
Lean.NameSet
source
instance
Lean
.
NameSet
.
instInhabitedNameSet
:
Inhabited
Lean.NameSet
source
def
Lean
.
NameSet
.
insert
(s :
Lean.NameSet
)
(n :
Lake.Name
)
:
Lean.NameSet
Instances For
source
def
Lean
.
NameSet
.
contains
(s :
Lean.NameSet
)
(n :
Lake.Name
)
:
Bool
Instances For
source
instance
Lean
.
NameSet
.
instForInNameSetName
{m :
Type
u_1 →
Type
u_2
}
:
ForIn
m
Lean.NameSet
Lake.Name
source
def
Lean
.
NameSSet
:
Type
Instances For
source
@[inline, reducible]
abbrev
Lean
.
NameSSet
.
empty
:
Lean.NameSSet
Instances For
source
instance
Lean
.
NameSSet
.
instEmptyCollectionNameSSet
:
EmptyCollection
Lean.NameSSet
source
instance
Lean
.
NameSSet
.
instInhabitedNameSSet
:
Inhabited
Lean.NameSSet
source
@[inline, reducible]
abbrev
Lean
.
NameSSet
.
insert
(s :
Lean.NameSSet
)
(n :
Lake.Name
)
:
Lean.NameSSet
Instances For
source
@[inline, reducible]
abbrev
Lean
.
NameSSet
.
contains
(s :
Lean.NameSSet
)
(n :
Lake.Name
)
:
Bool
Instances For
source
def
Lean
.
NameHashSet
:
Type
Instances For
source
@[inline]
def
Lean
.
NameHashSet
.
empty
:
Lean.NameHashSet
Instances For
source
instance
Lean
.
NameHashSet
.
instEmptyCollectionNameHashSet
:
EmptyCollection
Lean.NameHashSet
source
instance
Lean
.
NameHashSet
.
instInhabitedNameHashSet
:
Inhabited
Lean.NameHashSet
source
def
Lean
.
NameHashSet
.
insert
(s :
Lean.NameHashSet
)
(n :
Lake.Name
)
:
Lean.HashSet
Lake.Name
Instances For
source
def
Lean
.
NameHashSet
.
contains
(s :
Lean.NameHashSet
)
(n :
Lake.Name
)
:
Bool
Instances For
source
def
Lean
.
MacroScopesView
.
isPrefixOf
(v₁ :
Lean.MacroScopesView
)
(v₂ :
Lean.MacroScopesView
)
:
Bool
Instances For
source
def
Lean
.
MacroScopesView
.
isSuffixOf
(v₁ :
Lean.MacroScopesView
)
(v₂ :
Lean.MacroScopesView
)
:
Bool
Instances For