Nuprl Definition : branch
if p:P then A[p] else B fi == case d of inl(p) => A[p] | inr(x) => B
Definitions occuring in Statement :
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
branch
Latex:
if p:P then A[p] else B fi == case d of inl(p) => A[p] | inr(x) => B
Date html generated:
2016_05_15-PM-03_28_05
Last ObjectModification:
2015_09_23-AM-07_43_31
Theory : general
Home
Index