Nuprl Definition : prefix-replace

prefix-replace(t;x;pre) ==
  G(pre) where
  G(d<v>) = let d' = if name_eq(d;x) then t else d fi  in
             let v' = if name_eq(v;x) then t else v fi  in
             pisend(d';v')
  G(c?(w)) = let c' = if name_eq(c;x) then t else c fi  in
              let w' = if name_eq(w;x) then t else w fi  in
              pisend(c';w')

Definitions occuring in Statement : pi_prefix_ind: pi_prefix_ind, pisend: pisend(chan;var), name_eq: name_eq(x;y), ifthenelse: if b then t else f fi , let: let
FDL editor aliases : prefix-replace

Latex:
prefix-replace(t;x;pre) == G(pre) where G(d<v>) = let d' = if name\_eq(d;x) then t else d fi in let v' = if name\_eq(v;x) then t else v fi in pisend(d';v') G(c?(w)) = let c' = if name\_eq(c;x) then t else c fi in let w' = if name\_eq(w;x) then t else w fi in pisend(c';w') Date html generated: 2016_05_17-AM-11_24_27 Last ObjectModification: 2012_08_30-PM-01_18_51 Theory : event-logic-applications Home Index