Nuprl Definition : name-case

name-case(n;i,k.A[i; k];j,x.B[j; x]) ==
  case n of inl(ik) => let i,k:LocKnd = ik in A[i; k] | inr(p) => let j,x = p in B[j; x]


Definitions occuring in Statement :  locknd-spread: let i,k:LocKnd = ik in P[i; k],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :  name-case
name-case(n;i,k.A[i;  k];j,x.B[j;  x])  ==
    case  n  of  inl(ik)  =>  let  i,k:LocKnd  =  ik  in  A[i;  k]  |  inr(p)  =>  let  j,x  =  p  in  B[j;  x]


Date html generated: 2015_07_17-AM-09_14_56
Last ObjectModification: 2012_02_25-AM-10_53_58

Home Index