Documentation
Lean
.
Data
.
AssocList
Search
return to top
source
Imports
Init.Control.Id
Init.Data.List.Impl
Imported by
Lean
.
AssocList
Lean
.
instInhabitedAssocList
Lean
.
AssocList
.
empty
Lean
.
AssocList
.
instEmptyCollection
Lean
.
AssocList
.
insertNew
Lean
.
AssocList
.
isEmpty
Lean
.
AssocList
.
foldlM
Lean
.
AssocList
.
foldl
Lean
.
AssocList
.
toList
Lean
.
AssocList
.
forM
Lean
.
AssocList
.
mapKey
Lean
.
AssocList
.
mapVal
Lean
.
AssocList
.
findEntry?
Lean
.
AssocList
.
find?
Lean
.
AssocList
.
contains
Lean
.
AssocList
.
replace
Lean
.
AssocList
.
insert
Lean
.
AssocList
.
erase
Lean
.
AssocList
.
any
Lean
.
AssocList
.
all
Lean
.
AssocList
.
forIn
Lean
.
AssocList
.
forIn
.
loop
Lean
.
AssocList
.
instForInProd
List
.
toAssocList'
source
inductive
Lean
.
AssocList
(
α
:
Type
u)
(
β
:
Type
v)
:
Type
(max u v)
List-like type to avoid extra level of indirection
nil
{
α
:
Type
u}
{
β
:
Type
v}
:
AssocList
α
β
cons
{
α
:
Type
u}
{
β
:
Type
v}
(
key
:
α
)
(
value
:
β
)
(
tail
:
AssocList
α
β
)
:
AssocList
α
β
Instances For
source
instance
Lean
.
instInhabitedAssocList
{
a✝
:
Type
u_1}
{
a✝¹
:
Type
u_2}
:
Inhabited
(
AssocList
a✝
a✝¹
)
Equations
source
@[reducible, inline]
abbrev
Lean
.
AssocList
.
empty
{
α
:
Type
u}
{
β
:
Type
v}
:
AssocList
α
β
Equations
Instances For
source
instance
Lean
.
AssocList
.
instEmptyCollection
{
α
:
Type
u}
{
β
:
Type
v}
:
EmptyCollection
(
AssocList
α
β
)
Equations
source
@[reducible, inline]
abbrev
Lean
.
AssocList
.
insertNew
{
α
:
Type
u}
{
β
:
Type
v}
(
m
:
AssocList
α
β
)
(
k
:
α
)
(
v
:
β
)
:
AssocList
α
β
Equations
Instances For
source
def
Lean
.
AssocList
.
isEmpty
{
α
:
Type
u}
{
β
:
Type
v}
:
AssocList
α
β
→
Bool
Equations
Instances For
source
@[specialize #[]]
def
Lean
.
AssocList
.
foldlM
{
α
:
Type
u}
{
β
:
Type
v}
{
δ
:
Type
w}
{
m
:
Type
w →
Type
w
}
[
Monad
m
]
(
f
:
δ
→
α
→
β
→
m
δ
)
(
init
:
δ
)
:
AssocList
α
β
→
m
δ
Equations
Instances For
source
@[inline]
def
Lean
.
AssocList
.
foldl
{
α
:
Type
u}
{
β
:
Type
v}
{
δ
:
Type
w}
(
f
:
δ
→
α
→
β
→
δ
)
(
init
:
δ
)
(
as
:
AssocList
α
β
)
:
δ
Equations
Instances For
source
def
Lean
.
AssocList
.
toList
{
α
:
Type
u}
{
β
:
Type
v}
(
as
:
AssocList
α
β
)
:
List
(
α
×
β
)
Equations
Instances For
source
@[specialize #[]]
def
Lean
.
AssocList
.
forM
{
α
:
Type
u}
{
β
:
Type
v}
{
m
:
Type
w →
Type
w
}
[
Monad
m
]
(
f
:
α
→
β
→
m
PUnit
)
:
AssocList
α
β
→
m
PUnit
Equations
Instances For
source
def
Lean
.
AssocList
.
mapKey
{
α
:
Type
u}
{
β
:
Type
v}
{
δ
:
Type
w}
(
f
:
α
→
δ
)
:
AssocList
α
β
→
AssocList
δ
β
Equations
Instances For
source
def
Lean
.
AssocList
.
mapVal
{
α
:
Type
u}
{
β
:
Type
v}
{
δ
:
Type
w}
(
f
:
β
→
δ
)
:
AssocList
α
β
→
AssocList
α
δ
Equations
Instances For
source
def
Lean
.
AssocList
.
findEntry?
{
α
:
Type
u}
{
β
:
Type
v}
[
BEq
α
]
(
a
:
α
)
:
AssocList
α
β
→
Option
(
α
×
β
)
Equations
Instances For
source
def
Lean
.
AssocList
.
find?
{
α
:
Type
u}
{
β
:
Type
v}
[
BEq
α
]
(
a
:
α
)
:
AssocList
α
β
→
Option
β
Equations
Instances For
source
def
Lean
.
AssocList
.
contains
{
α
:
Type
u}
{
β
:
Type
v}
[
BEq
α
]
(
a
:
α
)
:
AssocList
α
β
→
Bool
Equations
Instances For
source
def
Lean
.
AssocList
.
replace
{
α
:
Type
u}
{
β
:
Type
v}
[
BEq
α
]
(
a
:
α
)
(
b
:
β
)
:
AssocList
α
β
→
AssocList
α
β
Equations
Instances For
source
def
Lean
.
AssocList
.
insert
{
α
:
Type
u}
{
β
:
Type
v}
[
BEq
α
]
(
m
:
AssocList
α
β
)
(
k
:
α
)
(
v
:
β
)
:
AssocList
α
β
Equations
Instances For
source
def
Lean
.
AssocList
.
erase
{
α
:
Type
u}
{
β
:
Type
v}
[
BEq
α
]
(
a
:
α
)
:
AssocList
α
β
→
AssocList
α
β
Equations
Instances For
source
def
Lean
.
AssocList
.
any
{
α
:
Type
u}
{
β
:
Type
v}
(
p
:
α
→
β
→
Bool
)
:
AssocList
α
β
→
Bool
Equations
Instances For
source
def
Lean
.
AssocList
.
all
{
α
:
Type
u}
{
β
:
Type
v}
(
p
:
α
→
β
→
Bool
)
:
AssocList
α
β
→
Bool
Equations
Instances For
source
@[inline]
def
Lean
.
AssocList
.
forIn
{
α
:
Type
u}
{
β
:
Type
v}
{
δ
:
Type
w}
{
m
:
Type
w →
Type
w'
}
[
Monad
m
]
(
as
:
AssocList
α
β
)
(
init
:
δ
)
(
f
:
α
×
β
→
δ
→
m
(
ForInStep
δ
)
)
:
m
δ
Equations
Instances For
source
@[specialize #[]]
def
Lean
.
AssocList
.
forIn
.
loop
{
α
:
Type
u}
{
β
:
Type
v}
{
δ
:
Type
w}
{
m
:
Type
w →
Type
w'
}
[
Monad
m
]
(
f
:
α
×
β
→
δ
→
m
(
ForInStep
δ
)
)
:
δ
→
AssocList
α
β
→
m
δ
Equations
Instances For
source
instance
Lean
.
AssocList
.
instForInProd
{
α
:
Type
u}
{
β
:
Type
v}
{
m
:
Type
w →
Type
w
}
:
ForIn
m
(
AssocList
α
β
)
(
α
×
β
)
Equations
source
def
List
.
toAssocList'
{
α
:
Type
u}
{
β
:
Type
v}
:
List
(
α
×
β
)
→
Lean.AssocList
α
β
Equations
Instances For