Nuprl Definition : spr_type
spr_type(g) == {f:
| 
x:. ((g mklist(x;f)) = 0)}
Definitions occuring in Statement :
nat: ,
all: x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
natural_number: $n,
equal: s = t,
mklist: mklist(n;f)
FDL editor aliases :
spr_type
spr\_type(g) == \{f:\mBbbN{} {}\mrightarrow{} \mBbbN{}| \mforall{}x:\mBbbN{}. ((g mklist(x;f)) = 0)\}
Date html generated:
2013_03_20-AM-10_32_35
Last ObjectModification:
2013_03_16-PM-04_02_11
Home
Index