mb
collection
Sections
GenAutomata
Doc
Def
x:A. B(x) == x:A
B(x)
is mentioned by
Thm*
c:Collection(T), f:(T
Collection(T')), y:T'. y
(
x
c.f(x))
(
x:T. x
c & y
f(x))
[member_col_accum]
Thm*
c:Collection(T), f:(T
T'), x:T'. x
< f(y) | y
c >
(
y:T. y
c & x = f(y))
[member_col_map]
Thm*
C:(I
Collection(T)), x:T. x
i:I. C(i)
(
i:I. x
C(i))
[member_col_union]
Def
(
x
c.f(x))(y) ==
x:T. x
c & y
f(x)
[col_accum]
Def
< f(x) | x
c > (y) ==
x:T. x
c & y = f(x)
T'
[col_map]
Def
(
i:I. C(i))(x) ==
i:I. x
C(i)
[col_union]
In prior sections:
core
fun
1
int
2
Try larger context:
GenAutomata
mb
collection
Sections
GenAutomata
Doc