Nuprl Definition : find-combine

find-combine(cmp;l) ==
  rec-case(l) of
  [] => inr ⋅ 
  a::as =>
   v.eval tst cmp in
     if (tst =z 0) then inl a
     if 0 <tst then inr ⋅ 
     else v

Definitions occuring in Statement :  list_ind: list_ind callbyvalue: callbyvalue ifthenelse: if then else fi  lt_int: i <j eq_int: (i =z j) it: apply: a inr: inr  inl: inl x natural_number: $n
Definitions occuring in definition :  list_ind: list_ind callbyvalue: callbyvalue apply: a eq_int: (i =z j) inl: inl x ifthenelse: if then else fi  lt_int: i <j natural_number: $n inr: inr  it:
FDL editor aliases :  find-combine

find-combine(cmp;l)  ==
    rec-case(l)  of
    []  =>  inr  \mcdot{} 
    a::as  =>
      v.eval  tst  =  cmp  a  in
          if  (tst  =\msubz{}  0)  then  inl  a
          if  0  <z  tst  then  inr  \mcdot{} 
          else  v

Date html generated: 2016_05_14-PM-02_40_01
Last ObjectModification: 2015_09_22-PM-05_57_08

Theory : list_1

Home Index