Nuprl Definition : face-complex
face-complex(k;L) == remove-repeats(rc-deq(k);concat(map(λc.if Inhabited(c) then rat-cube-faces(k;c) else [] fi ;L)))
Definitions occuring in Statement :
rat-cube-faces: rat-cube-faces(k;c),
inhabited-rat-cube: Inhabited(c),
rc-deq: rc-deq(k),
remove-repeats: remove-repeats(eq;L),
concat: concat(ll),
map: map(f;as),
nil: [],
ifthenelse: if b then t else f fi ,
lambda: λx.A[x]
Definitions occuring in definition :
nil: [],
rat-cube-faces: rat-cube-faces(k;c),
inhabited-rat-cube: Inhabited(c),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
map: map(f;as),
concat: concat(ll),
rc-deq: rc-deq(k),
remove-repeats: remove-repeats(eq;L)
FDL editor aliases :
face-complex
Latex:
face-complex(k;L) ==
remove-repeats(rc-deq(k);concat(map(\mlambda{}c.if Inhabited(c) then rat-cube-faces(k;c) else [] fi ;L)))
Date html generated:
2019_10_29-AM-07_57_40
Last ObjectModification:
2019_10_18-PM-00_04_50
Theory : rationals
Home
Index