Nuprl Definition : list-ss
list(ss) ==
Point=Point(ss) List #=λp,q. if ||p||=||q|| then ∃i:ℕ||p||. p[i] # q[i] else True
cotrans=λp,q,r,sep. if ||p||=||q||
then if ||q||=||r||
then let i,x = sep
in case ss."#or" p[i] q[i] r[i] x of inl(a) => inl <i, a> | inr(a) => inr <i, a>
else (inr Ax )
else if ||q||=||r|| then inl Ax else (inr Ax )
Definitions occuring in Statement :
mk-ss: Point=P #=Sep cotrans=C,
ss-sep: x # y,
ss-point: Point(ss),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
exists: ∃x:A. B[x],
true: True,
int_eq: if a=b then c else d,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
natural_number: $n,
token: "$token",
axiom: Ax,
record-select: r.x
Definitions occuring in definition :
mk-ss: Point=P #=Sep cotrans=C,
list: T List,
ss-point: Point(ss),
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
ss-sep: x # y,
true: True,
lambda: λx.A[x],
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
record-select: r.x,
token: "$token",
select: L[n],
pair: <a, b>,
int_eq: if a=b then c else d,
length: ||as||,
inl: inl x,
inr: inr x ,
axiom: Ax
FDL editor aliases :
list-ss
Latex:
list(ss) ==
Point=Point(ss) List \#=\mlambda{}p,q. if ||p||=||q|| then \mexists{}i:\mBbbN{}||p||. p[i] \# q[i] else True
cotrans=\mlambda{}p,q,r,sep. if ||p||=||q||
then if ||q||=||r||
then let i,x = sep
in case ss."\#or" p[i] q[i] r[i] x
of inl(a) =>
inl <i, a>
| inr(a) =>
inr <i, a>
else (inr Ax )
else if ||q||=||r|| then inl Ax else (inr Ax )
Date html generated:
2019_10_31-AM-07_27_06
Last ObjectModification:
2019_09_19-PM-04_12_05
Theory : constructive!algebra
Home
Index