The file algebra/domain.spad.pamphlet
contains this definition:
)abbrev domain CATEGORY Category
++ Author: Gabriel Dos Reis
++ Date Create: February 16, 2008.
++ Date Last Updated: February 16, 2008.
++ Basic Operations: coerce
...
but OpenAxiom? does not always treat Category
this way:
axiom
)show Category
Category is a domain constructor
Abbreviation for Category is CATEGORY
This constructor is not exposed in this frame.
Issue )edit /usr/local/lib/open-axiom/x86_64-unknown-
linux/1.2.0-2008-05-25/src/algebra/CATEGORY.spad to see algebra source code for
CATEGORY
------------------------------- Operations --------------------------------
coerce : % -> OutputForm
Type: Type
axiom
x:Category
Category is a category, not a domain, and declarations require
domains.
axiom
Category has Category
Type: Boolean
Type: Boolean
Type: Boolean
Axiom Version: => /usr/local/lib/open-axiom/x86_64-unknown-linux/1.2.0-2008-05-25
hat is a regression, because the rest of the compiler and interpreter
assumes that Category is conceptually a category -- even when it has a
domain implementation.
gdr wrote:
Category is conceptually a category -- even when it has a domain implementation
Could you please explain what that means? :-)
At the conceptual level, OpenAixom
? thinks of Category as a category. The
category of categories. However, it has a domain implementation, e.g.
as reported by )show. That is just an implementation detail.
OpenAxiom
? trunk as of 2008-05-29 says this:
(1) -> Category has Category
(1) ->
(1) true
Type: Boolean
(2) -> Domain has Category
(2) ->
(2) true
Type: Boolean
(3) -> Category has Type
(3) ->
<a href="#eq3">(3)</a> true
Type: Boolean