Nuprl Definition : prior-as-rec-bind-class-in
prior-as-rec-bind-class-in(X;i) ==
case i
of inl(b) =>
Null
| inr(x) =>
case x of inl(b) => (Skip(send-class({b})) until Skip(X)) (+) Null | inr(u) => Null (+) Lift(X) (+) Null
Definitions occuring in Statement :
send-class: send-class(b)
,
lift-class: Lift(X)
,
null-class: Null
,
disjoint-union-comb: X (+) Y
,
skip-first-class: Skip(X)
,
until-class: (X until Y)
,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
,
single-bag: {x}
FDL editor aliases :
prior-as-rec-bind-class-in
Latex:
prior-as-rec-bind-class-in(X;i) ==
case i
of inl(b) =>
Null
| inr(x) =>
case x
of inl(b) =>
(Skip(send-class(\{b\})) until Skip(X)) (+) Null
| inr(u) =>
Null (+) Lift(X) (+) Null
Date html generated:
2015_07_21-PM-03_13_42
Last ObjectModification:
2012_04_15-PM-04_40_32
Home
Index