Nuprl Definition : listp
A List+ == {l:A List| 0 < ||l||}
Definitions occuring in Statement :
length: ||as||,
list: T List,
less_than: a < b,
set: {x:A| B[x]} ,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
list: T List,
less_than: a < b,
natural_number: $n,
length: ||as||
FDL editor aliases :
listp
Latex:
A List\msupplus{} == \{l:A List| 0 < ||l||\}
Date html generated:
2016_05_14-AM-06_34_52
Last ObjectModification:
2015_12_03-PM-02_06_35
Theory : list_0
Home
Index