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