Nuprl Definition : index-min

index-min(zs) ==
  rec-case(zs) of
  [] => <0, 0>
  z::more =>
   p.if more = Ax then <0, z> otherwise let i,x = p 
                      in if (z) < (x)  then <0, z>  else eval j = i + 1 in <j, x>


Definitions occuring in Statement :  list_ind: list_ind,  callbyvalue: callbyvalue,  isaxiom: if z = Ax then a otherwise b,  less: if (a) < (b)  then c  else d,  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n
Definitions occuring in definition :  list_ind: list_ind,  isaxiom: if z = Ax then a otherwise b,  spread: spread def,  less: if (a) < (b)  then c  else d,  callbyvalue: callbyvalue,  add: n + m,  natural_number: $n,  pair: <a, b>
FDL editor aliases :  index-min
Latex:
index-min(zs)  ==
    rec-case(zs)  of
    []  =>  ɘ,  0>
    z::more  =>
      p.if  more  =  Ax  then  ɘ,  z>  otherwise  let  i,x  =  p 
                                            in  if  (z)  <  (x)    then  ɘ,  z>    else  eval  j  =  i  +  1  in  <j,  x>


Date html generated: 2016_05_14-AM-06_55_22
Last ObjectModification: 2015_12_22-AM-08_20_53

Theory : omega


Home Index