Nuprl Definition : poly-coeff-of

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

Definitions occuring in Statement :  intlex: l1 ≤_lex l2 list_ind: list_ind ifthenelse: if then else fi  spread: spread def natural_number: $n
Definitions occuring in definition :  list_ind: list_ind spread: spread def ifthenelse: if then else fi  intlex: l1 ≤_lex l2 natural_number: $n
FDL editor aliases :  poly-coeff-of

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