Nuprl Definition : find-exact-eq-constraint

find-exact-eq-constraint(L) ==
  let a,as = L 
  in case test-exact-eq-constraint(as) of inl(n) => inl <L, n + 1> | inr(x) => inr x 


Definitions occuring in Statement :  test-exact-eq-constraint: test-exact-eq-constraint(L),  spread: spread def,  pair: <a, b>,  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 :  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  test-exact-eq-constraint: test-exact-eq-constraint(L),  inl: inl x,  pair: <a, b>,  add: n + m,  natural_number: $n,  inr: inr x 
FDL editor aliases :  find-exact-eq-constraint
Latex:
find-exact-eq-constraint(L)  ==
    let  a,as  =  L 
    in  case  test-exact-eq-constraint(as)  of  inl(n)  =>  inl  <L,  n  +  1>  |  inr(x)  =>  inr  x 


Date html generated: 2016_05_14-AM-07_16_49
Last ObjectModification: 2015_09_22-PM-05_53_31

Theory : omega


Home Index