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