Nuprl Definition : vec
vec(T;n) == {L:T List| ||L|| = n ∈ ℤ}
Definitions occuring in Statement :
length: ||as||,
list: T List,
set: {x:A| B[x]} ,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
list: T List,
equal: s = t ∈ T,
int: ℤ,
length: ||as||
FDL editor aliases :
vec
Latex:
vec(T;n) == \{L:T List| ||L|| = n\}
Date html generated:
2016_05_14-PM-03_31_16
Last ObjectModification:
2015_09_22-PM-06_00_38
Theory : decidable!equality
Home
Index