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