Nuprl Definition : mrec_ind
mrec_ind(L;h;x) ==
let i,x1 = x
in letrec r(i)=λx.(h i (fst(x)) (snd(x))
let L' = case apply-alist(AtomDeq;L;i)
of inl(L2) =>
case apply-alist(AtomDeq;L2;fst(x)) of inl(as) => as | inr(_) => Ax
| inr(_) =>
Ax in
λj.case L'[j]
of inl(x@0) =>
case x@0 of inl(x1) => r x1 snd(x).j | inr(y) => λi@0.(r y snd(x).j[i@0])
| inr(y) =>
Ax) in
r(i)
x1
Definitions occuring in Statement :
select-tuple: x.n,
apply-alist: apply-alist(eq;L;x),
select: L[n],
length: ||as||,
atom-deq: AtomDeq,
genrec-ap: genrec-ap,
let: let,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
axiom: Ax
Definitions occuring in definition :
spread: spread def,
genrec-ap: genrec-ap,
let: let,
apply-alist: apply-alist(eq;L;x),
atom-deq: AtomDeq,
pi1: fst(t),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
lambda: λx.A[x],
apply: f a,
select: L[n],
select-tuple: x.n,
length: ||as||,
pi2: snd(t),
axiom: Ax
FDL editor aliases :
mrec_ind
Latex:
mrec\_ind(L;h;x) ==
let i,x1 = x
in letrec r(i)=\mlambda{}x.(h i (fst(x)) (snd(x))
let L' = case apply-alist(AtomDeq;L;i)
of inl(L2) =>
case apply-alist(AtomDeq;L2;fst(x)) of inl(as) => as | inr($_\000C{}$) => Ax
| inr($_{}$) =>
Ax in
\mlambda{}j.case L'[j]
of inl(x@0) =>
case x@0
of inl(x1) =>
r x1 snd(x).j
| inr(y) =>
\mlambda{}i@0.(r y snd(x).j[i@0])
| inr(y) =>
Ax) in
r(i)
x1
Date html generated:
2019_06_20-PM-02_16_21
Last ObjectModification:
2019_02_28-PM-06_07_55
Theory : tuples
Home
Index