Nuprl Definition : run-cause

run-cause(r) ==  λe.let t,x = fst(run-info(r;e)) in if 0 ≤z t ∧b is-run-event(r;t;x) then inl <t, x> else inr ⋅  fi 


Definitions occuring in Statement :  run-info: run-info(r;e),  is-run-event: is-run-event(r;t;x),  le_int: i ≤z j,  band: p ∧b q,  ifthenelse: if b then t else f fi ,  it: ⋅,  pi1: fst(t),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x,  natural_number: $n
FDL editor aliases :  run-cause
Latex:
run-cause(r)  ==
    \mlambda{}e.let  t,x  =  fst(run-info(r;e)) 
          in  if  0  \mleq{}z  t  \mwedge{}\msubb{}  is-run-event(r;t;x)  then  inl  <t,  x>  else  inr  \mcdot{}    fi 


Date html generated: 2015_07_23-AM-11_13_52
Last ObjectModification: 2012_02_25-PM-03_42_30

Home Index