mb
collection
Sections
GenAutomata
Doc
Def
||as|| == Case of as; nil
0 ; a.as'
||as'||+1 (recursive)
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:
list
1
Try larger context:
GenAutomata
mb
collection
Sections
GenAutomata
Doc