mb
collection
Sections
GenAutomata
Doc
Def
== {i:
| 0
i }
is mentioned by
Thm*
l:Collection(T) List, x:T List. x
col_list_prod(l)
||x|| = ||l||
& (
i:
. i < ||x||
x[i]
l[i])
[member_col_list_prod]
Def
col_list_prod(l)(x) == ||x|| = ||l||
& (
i:
. i < ||x||
x[i]
l[i])
[col_list_prod]
In prior sections:
int
1
bool
1
int
2
list
1
Try larger context:
GenAutomata
mb
collection
Sections
GenAutomata
Doc