Nuprl Definition : geo-primitives
GeometryPrimitives == "Point":Type"O":Point ⟶ Point ⟶ Point ⟶ Point ⟶ ℙ"L":Point ⟶ Point ⟶ Point ⟶ ℙ
Definitions occuring in Statement :
geo-point: Point,
top: Top,
prop: ℙ,
function: x:A ⟶ B[x],
token: "$token",
universe: Type,
record+: record+,
record: record(x.T[x])
Definitions occuring in definition :
prop: ℙ,
geo-point: Point,
function: x:A ⟶ B[x],
token: "$token",
universe: Type,
top: Top,
record: record(x.T[x]),
record+: record+
FDL editor aliases :
geo-primitives
geo-prim
Latex:
GeometryPrimitives ==
"Point":Type
"O":Point {}\mrightarrow{} Point {}\mrightarrow{} Point {}\mrightarrow{} Point {}\mrightarrow{} \mBbbP{}
"L":Point {}\mrightarrow{} Point {}\mrightarrow{} Point {}\mrightarrow{} \mBbbP{}
Date html generated:
2019_10_29-AM-09_11_47
Last ObjectModification:
2019_10_25-PM-00_57_16
Theory : euclidean!plane!geometry
Home
Index