mb
collection
Sections
GenAutomata
Doc
Def
l[i] == hd(nth_tl(i;l))
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