Nuprl Definition : mrec-spec

mrec-spec(L;lbl;p) ==
  case apply-alist(AtomDeq;L;p)
   of inl(L2) =>
   case apply-alist(AtomDeq;L2;lbl) of inl(as) => as | inr(_) => []
   | inr(_) =>
   []

Definitions occuring in Statement : apply-alist: apply-alist(eq;L;x), nil: [], atom-deq: AtomDeq, decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : decide: case b of inl(x) => s[x] | inr(y) => t[y], apply-alist: apply-alist(eq;L;x), atom-deq: AtomDeq, nil: []
FDL editor aliases : mrec-spec

Latex:
mrec-spec(L;lbl;p) == case apply-alist(AtomDeq;L;p) of inl(L2) => case apply-alist(AtomDeq;L2;lbl) of inl(as) => as | inr($_{}$) => [] | inr($_{}$) => [] Date html generated: 2019_06_20-PM-02_14_38 Last ObjectModification: 2019_02_24-PM-10_11_23 Theory : tuples Home Index