Nuprl Definition : vec

vec(T;n) ==  {L:T List| ||L|| n ∈ ℤ



Definitions occuring in Statement :  length: ||as|| list: List set: {x:A| B[x]}  int: equal: t ∈ T
Definitions occuring in definition :  set: {x:A| B[x]}  list: List equal: 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