Nuprl Definition : select-last-in-nat-missing

select-last-in-nat-missing(max;missing) ==
  primrec(max;if in-missing(0;missing) then -1 else 0 fi ;λm,r. if in-missing(m;missing) then r else m fi )


Definitions occuring in Statement :  in-missing: in-missing(i;missing),  primrec: primrec(n;b;c),  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  minus: -n,  natural_number: $n
FDL editor aliases :  select-last-in-nat-missing
select-last-in-nat-missing(max;missing)  ==
    primrec(max;if  in-missing(0;missing)  then  -1  else  0  fi  ;\mlambda{}m,r.  if  in-missing(m;missing)
                                                                                                                              then  r
                                                                                                                              else  m
                                                                                                                              fi  )


Date html generated: 2015_07_17-AM-08_21_41
Last ObjectModification: 2013_04_02-PM-01_31_34

Home Index