Nuprl Definition : decide def
case b of inl(x) => s[x] | inr(y) => t[y] == PRIMITIVE
Rules referencing :
unionElimination,
decideEquality,
equalityEqualityBase,
callbyvalueDecide,
decideExceptionCases,
orFunctionality
Latex:
case b of inl(x) => s[x] | inr(y) => t[y] == PRIMITIVE
Date html generated:
2016_05_13-PM-03_03_52
Last ObjectModification:
2006_01_26-PM-03_54_17
Theory : core_1
Home
Index