Nuprl Definition : test-exact-eq-constraint

test-exact-eq-constraint(L) ==
  rec-case(L) of
  [] => inr ⋅ 
  a::as =>
   r.if (|a| =z 1) then inl 0 else case r of inl(n) => inl (n + 1) | inr(x) => inr x  fi 


Definitions occuring in Statement :  list_ind: list_ind,  absval: |i|,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  it: ⋅,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n
Definitions occuring in definition :  list_ind: list_ind,  it: ⋅,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  absval: |i|,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inl: inl x,  add: n + m,  natural_number: $n,  inr: inr x 
FDL editor aliases :  test-exact-eq-constraint
Latex:
test-exact-eq-constraint(L)  ==
    rec-case(L)  of
    []  =>  inr  \mcdot{} 
    a::as  =>
      r.if  (|a|  =\msubz{}  1)  then  inl  0  else  case  r  of  inl(n)  =>  inl  (n  +  1)  |  inr(x)  =>  inr  x    fi 


Date html generated: 2016_05_14-AM-07_16_41
Last ObjectModification: 2015_09_22-PM-05_53_29

Theory : omega


Home Index