Nuprl Definition : es-pred

pred(e) ==  fix((λes-pred,e. let p = pred1(e) in if es-dom(es) p then p if es-eq(es) p e then e else es-pred p fi )) e


Definitions occuring in Statement :  es-eq: es-eq(es),  es-base-pred: pred1(e),  es-dom: es-dom(es),  ifthenelse: if b then t else f fi ,  let: let,  apply: f a,  fix: fix(F),  lambda: λx.A[x]
FDL editor aliases :  es-pred es-pred
pred(e)  ==
    fix((\mlambda{}es-pred,e.  let  p  =  pred1(e)  in
                                              if  es-dom(es)  p  then  p
                                              if  es-eq(es)  p  e  then  e
                                              else  es-pred  p
                                              fi  )) 
    e


Date html generated: 2015_07_17-AM-08_35_01
Last ObjectModification: 2013_03_23-PM-05_08_51

Home Index