Nuprl Definition : destructor
destructor{i:l}(T.F[T]) == ⋂T:{T:Type| T ⊆r Base} . (x:F[T] ⟶ decomp{i:l}(T.F[T];T;x))
Definitions occuring in Statement :
decomp: decomp{i:l}(S.F[S];T;x),
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],
decomp: decomp{i:l}(S.F[S];T;x)
FDL editor aliases :
destructor
Latex:
destructor\{i:l\}(T.F[T]) == \mcap{}T:\{T:Type| T \msubseteq{}r Base\} . (x:F[T] {}\mrightarrow{} decomp\{i:l\}(T.F[T];T;x))
Date html generated:
2016_05_15-PM-06_56_34
Last ObjectModification:
2015_09_23-AM-08_08_07
Theory : general
Home
Index