Nuprl Definition : prec-arg-types

prec-arg-types(lbl,p.a[lbl; p];i;lbl) ==
  map(λx.case x
          of inl(y) =>
          case y of inl(p) => prec(lbl,p.a[lbl; p];p) | inr(p) => prec(lbl,p.a[lbl; p];p) List
          | inr(E) =>
          E;a[lbl; i])

Definitions occuring in Statement : prec: prec(lbl,p.a[lbl; p];i), map: map(f;as), list: T List, lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : map: map(f;as), lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y], list: T List, prec: prec(lbl,p.a[lbl; p];i)
FDL editor aliases : prec-arg-types

Latex:
prec-arg-types(lbl,p.a[lbl; p];i;lbl) == map(\mlambda{}x.case x of inl(y) => case y of inl(p) => prec(lbl,p.a[lbl; p];p) | inr(p) => prec(lbl,p.a[lbl; p];p) List | inr(E) => E;a[lbl; i]) Date html generated: 2019_06_20-PM-02_05_09 Last ObjectModification: 2019_02_22-PM-06_23_26 Theory : tuples Home Index