Nuprl Definition : poly-coeff-of

poly-coeff-of(vs;p) ==
  rec-case(p) of
  [] => 0
  m::ps2 =>
   r.let c,ws = m 
     in if ws ≤_lex vs then if vs ≤_lex ws then c else r fi  else 0 fi 


Definitions occuring in Statement :  intlex: l1 ≤_lex l2,  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  spread: spread def,  natural_number: $n
Definitions occuring in definition :  list_ind: list_ind,  spread: spread def,  ifthenelse: if b then t else f fi ,  intlex: l1 ≤_lex l2,  natural_number: $n
FDL editor aliases :  poly-coeff-of
Latex:
poly-coeff-of(vs;p)  ==
    rec-case(p)  of
    []  =>  0
    m::ps2  =>
      r.let  c,ws  =  m 
          in  if  ws  \mleq{}\_lex  vs  then  if  vs  \mleq{}\_lex  ws  then  c  else  r  fi    else  0  fi 


Date html generated: 2016_05_14-AM-07_10_35
Last ObjectModification: 2015_09_22-PM-05_53_07

Theory : omega


Home Index