Nuprl Definition : is-exception
Howe's `sqle` relation is enough to define the proposition
(about t ∈ Base) that t is an exception.
Note that this is not a decidable proposition!
If being an exception were decidable, then a program could
catch *all* exceptions and we would not be able
to use exceptions to find the modulus of continuity of functionals.
The test ⌜isaxiom(e?n:x.Ax) ∧b isint(e?n:x.2)⌝ can be used to distinguish between
canonical values that are not exceptions and exceptions *with name n*.
But on other exceptions e', this test will raise the exception e'
(as it must, for our construction of the modulus of continuity to work.)
⋅
is-exception(t) == exception(⊥; ⊥) ≤ t
Definitions occuring in Statement :
sqle: s ≤ t
Definitions occuring in definition :
sqle: s ≤ t
Rules referencing :
divergentSqle,
divergentSqlen,
exceptionSqequal,
ispairExceptionCases,
isintExceptionCases,
isaxiomExceptionCases,
isatomExceptionCases,
isinlExceptionCases,
isinrExceptionCases,
islambdaExceptionCases,
isatom1ExceptionCases,
isatom2ExceptionCases,
decideExceptionCases,
spreadExceptionCases,
minusExceptionCases,
applyExceptionCases,
int_eqExceptionCases,
lessExceptionCases,
atom_eqExceptionCases,
atom1_eqExceptionCases,
atom2_eqExceptionCases,
addExceptionCases,
divideExceptionCases,
remainderExceptionCases,
multiplyExceptionCases,
callbyvalueExceptionCases
FDL editor aliases :
is-exception
Latex:
is-exception(t) == exception(\mbot{}; \mbot{}) \mleq{} t
Date html generated:
2016_07_08-PM-04_46_54
Last ObjectModification:
2015_09_22-PM-05_44_33
Theory : call!by!value_1
Home
Index