Nuprl Definition : ndlist
ndlist(T) == {L:T List| no_repeats(T;L)}
Definitions occuring in Statement :
no_repeats: no_repeats(T;l),
list: T List,
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
list: T List,
no_repeats: no_repeats(T;l)
FDL editor aliases :
ndlist
Latex:
ndlist(T) == \{L:T List| no\_repeats(T;L)\}
Date html generated:
2016_05_14-PM-03_31_02
Last ObjectModification:
2015_09_22-PM-06_00_33
Theory : decidable!equality
Home
Index