Nuprl Definition : choicef
∈x:T. P[x] == case xm {y:T| P[y]} of inl(z) => z | inr(w) => "???"
Definitions occuring in Statement :
set: {x:A| B[x]} ,
apply: f a,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
token: "$token"
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
set: {x:A| B[x]} ,
token: "$token"
FDL editor aliases :
choicef
Latex:
\mmember{}x:T. P[x] == case xm \{y:T| P[y]\} of inl(z) => z | inr(w) => "???"
Date html generated:
2016_05_13-PM-03_14_54
Last ObjectModification:
2016_01_04-AM-10_26_29
Theory : core_2
Home
Index