Nuprl Definition : has-value
If ⌜a⌝ has a value then the call-by-value term
⌜eval a; 0⌝ evaluates to 0. If ⌜a⌝ diverges then so does ⌜eval a; 0⌝.
Thus, ⌜a⌝ has a value if and only if ⌜0 ≤ eval a; 0⌝⋅
(a)↓ == 0 ≤ eval a; 0
Definitions occuring in Statement :
callbyvalue: callbyvalue,
natural_number: $n,
sqle: s ≤ t
Definitions occuring in definition :
sqle: s ≤ t,
callbyvalue: callbyvalue,
natural_number: $n
Rules referencing :
divergentSqle,
divergentSqlen,
compactness,
callbyvalueApply,
callbyvalueApplyCases,
exceptionApplyCases,
sqleLambda,
callbyvalueCallbyvalue,
callbyvalueIspair,
callbyvalueIsaxiom,
callbyvalueIsinl,
callbyvalueIsinr,
callbyvalueIslambda,
callbyvalueIsint,
callbyvalueIsatom,
callbyvalueIsatom1,
callbyvalueIsatom2,
ispairExceptionCases,
isintExceptionCases,
isaxiomExceptionCases,
isatomExceptionCases,
isinlExceptionCases,
isinrExceptionCases,
islambdaExceptionCases,
isatom1ExceptionCases,
isatom2ExceptionCases,
applyExceptionCases,
callbyvalueExceptionCases,
bottomDivergent
FDL editor aliases :
has-value
Latex:
(a)\mdownarrow{} == 0 \mleq{} eval a; 0
Date html generated:
2016_07_08-PM-04_46_56
Last ObjectModification:
2015_09_22-PM-05_44_34
Theory : call!by!value_1
Home
Index