login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for SandboxTypeDefinitions revision 2 of 15

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Editor: hemmecke
Time: 2008/07/08 02:51:56 GMT-7
Note:

changed:
-  A **category** is a type whose type is the language-defined constant Category.
-
-  A **domain** is a type whose type is a category.
-
-  A **type** is either a category, a domain or the language-defined constants Category and Type.
-
-  Any **type** is of type Type.
  A **category** is an L-type whose type is the language-defined constant 'Category'.

  A **domain** is an L-type whose type is a category.

  An **L-type** is either a category, a domain or the language-defined constants 'Category' and 'Type'.

  Any L-type is of type 'Type'.

  I wrote **L-type** to mean *type in the language*, either Aldor or SPAD.

There seems to be different understandings of Type, domain, category, Category, etc. around. Here is an attempt to collect all these different opinions in order to make discussion about them clearer.

Definitions of Ralf Hemmecke

A category is an L-type whose type is the language-defined constant Category.

A domain is an L-type whose type is a category.

An L-type is either a category, a domain or the language-defined constants Category and Type.

Any L-type is of type Type.

I wrote L-type to mean type in the language, either Aldor or SPAD.