---

prop-rule-realizer-out(T;x;f;g;hdr) ==
  z.case z
     of inl(v) => make-lg(map(y.<y, "msg", hdr, T, f x v>;g v))
      | inr(v) => lg-nil()

---

Definitions :  lg-nil: lg-nil(),  apply: f a,  pair: <a, b>,  token: "$token",  lambda: x.A[x],  map: map(f;as),  make-lg: make-lg(L),  decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :  prop-rule-realizer-out

---

prop-rule-realizer-out(T;x;f;g;hdr)  ==
    \mlambda{}z.case  z  of  inl(v)  =>  make-lg(map(\mlambda{}y.<y,  "msg",  hdr,  T,  f  x  v>g  v))  |  inr(v)  =>  lg-nil()


Date html generated: 2010_08_30-AM-12_55_30
Last ObjectModification: 2010_08_23-PM-12_33_36

Home Index