Nuprl Definition : aa_max_w

Nuprl Definition : aa_max_w_unit

aa_max_w_unit(u1;u2) ==
  case u1
  of inl(intval1) =>
   case u2 of inl(intval2) => inl imax(intval1;intval2)  | inr(unitval2) => u1
   | inr(unitval1) =>
   u2

Definitions occuring in Statement : imax: imax(a;b), decide: case b of inl(x) => s[x] | inr(y) => t[y], inl: inl x
FDL editor aliases : aa_max_w_unit
aa\_max\_w\_unit(u1;u2) == case u1 of inl(intval1) => case u2 of inl(intval2) => inl imax(intval1;intval2) | inr(unitval2) => u1 | inr(unitval1) => u2 Date html generated: 2013_03_20-AM-09_52_09 Last ObjectModification: 2012_11_27-AM-10_32_15 Home Index