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