Nuprl Definition : Exception
The type of terms that are exceptions with name n and values in type T.
Exception(n;T) == {t:Base| exception-with-name(n;t) ∧ (exception-value(n;t) ∈ T)}
Definitions occuring in Statement :
exception-value: exception-value(n;t),
exception-with-name: exception-with-name(n;t),
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
base: Base
Definitions occuring in definition :
set: {x:A| B[x]} ,
base: Base,
and: P ∧ Q,
exception-with-name: exception-with-name(n;t),
member: t ∈ T,
exception-value: exception-value(n;t)
FDL editor aliases :
Exception
Latex:
Exception(n;T) == \{t:Base| exception-with-name(n;t) \mwedge{} (exception-value(n;t) \mmember{} T)\}
Date html generated:
2016_07_08-PM-04_46_54
Last ObjectModification:
2015_09_22-PM-05_44_34
Theory : call!by!value_1
Home
Index