Nuprl Definition : hull-cmp
hull-cmp(g;xs;i;j) == λx,y. if (x =z y) then 0 if y L ix then 1 else -1 fi
Definitions occuring in Statement :
left-test: i L jk,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x],
minus: -n,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
eq_int: (i =z j),
ifthenelse: if b then t else f fi ,
left-test: i L jk,
minus: -n,
natural_number: $n
FDL editor aliases :
hull-cmp
Latex:
hull-cmp(g;xs;i;j) == \mlambda{}x,y. if (x =\msubz{} y) then 0 if y L ix then 1 else -1 fi
Date html generated:
2017_10_02-PM-06_52_20
Last ObjectModification:
2017_08_06-PM-07_32_00
Theory : euclidean!plane!geometry
Home
Index