Nuprl Definition : ifthenelse
if b then t else f fi == case b of inl() => t | inr() => f
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 :
ifthenelse
Latex:
if b then t else f fi == case b of inl() => t | inr() => f
Date html generated:
2016_05_13-PM-03_20_16
Last ObjectModification:
2016_01_04-AM-10_27_18
Theory : union
Home
Index