Nuprl Definition : ut1-test
ut1-test{$aaa,$bbb}(x) == case x of inl(a) => '$aaa'1 | inr(b) => '$bbb'1
Definitions occuring in Statement :
token: '$x'1,
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],
token: '$x'1
FDL editor aliases :
ut1-test
Latex:
ut1-test\{\$aaa,\$bbb\}(x) == case x of inl(a) => '\$aaa'1 | inr(b) => '\$bbb'1
Date html generated:
2016_05_15-PM-07_57_08
Last ObjectModification:
2015_09_23-AM-08_20_30
Theory : general
Home
Index