Nuprl Definition : es-rec-class

RecClass(first e
           G[es; e]
         or next e after e' with value v
             F[es; e'; v; e]) ==
  fix((λes-rec-class,es,e. if e ∈b prior(es-rec-class)
                          then let e' = prior(es-rec-class)(e) in
                                   F[es; e'; es-rec-class(e'); e]
                          else G[es; e]
                          fi ))


Definitions occuring in Statement :  es-prior-interface: prior(X),  eclass-val: X(e),  in-eclass: e ∈b X,  ifthenelse: if b then t else f fi ,  let: let,  fix: fix(F),  lambda: λx.A[x]
FDL editor aliases :  es-rec-class
Latex:
RecClass(first  e
                      G[es;  e]
                  or  next  e  after  e'  with  value  v
                          F[es;  e';  v;  e])  ==
    fix((\mlambda{}es-rec-class,es,e.  if  e  \mmember{}\msubb{}  prior(es-rec-class)
                                                    then  let  e'  =  prior(es-rec-class)(e)  in
                                                                      F[es;  e';  es-rec-class(e');  e]
                                                    else  G[es;  e]
                                                    fi  ))


Date html generated: 2015_07_21-PM-03_17_03
Last ObjectModification: 2012_07_02-PM-04_13_21

Home Index