Nuprl Definition : constructor
Constr(T.F[T]) == ⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T])
Definitions occuring in Statement :
list: T List,
subtype_rel: A ⊆r B,
set: {x:A| B[x]} ,
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
base: Base,
universe: Type
Definitions occuring in definition :
isect: ⋂x:A. B[x],
set: {x:A| B[x]} ,
universe: Type,
subtype_rel: A ⊆r B,
base: Base,
function: x:A ⟶ B[x],
list: T List
FDL editor aliases :
constructor
Latex:
Constr(T.F[T]) == \mcap{}T:\{T:Type| T \msubseteq{}r Base\} . ((T List) {}\mrightarrow{} F[T])
Date html generated:
2016_05_15-PM-06_55_07
Last ObjectModification:
2015_09_23-AM-08_07_33
Theory : general
Home
Index