knownInfo (conditionals in categories)

[Ralf Hemmecke]

Unfortunately the compiler does compile the Cat category, but
it cannot compile the domains.

Do I also have to lie about the exports as it is done in other part of
the library, for example here:

https://github.com/fricas/fricas/blob/master/src/algebra/catdef.spad#L329

?

Ralf

-----------------------------------------------------------

)abbrev category CAT Cat
Cat(S: SetCategory): Category == with
if S is Integer then foo: () -> Integer

)abbrev domain DOM1 Dom1
Dom1(S: SetCategory): Cat S with
bar: () -> Integer
== add
if S is Integer then foo(): Integer == 1
bar(): Integer == 1

)abbrev domain DOM2 Dom2
Dom2(S: SetCategory): with
if S is Integer then foo: () -> Integer
bar: () -> Integer
== add
if S is Integer then foo(): Integer == 1
bar(): Integer == 1

[Waldek Hebisch]

On Mon, Dec 08, 2025 at 05:32:45PM +0100, 'Ralf Hemmecke' via FriCAS - computer algebra system wrote:
> Unfortunately the compiler does compile the Cat category, but
> it cannot compile the domains.
>
> Do I also have to lie about the exports as it is done in other part of the
> library, for example here:
>
> https://github.com/fricas/fricas/blob/master/src/algebra/catdef.spad#L329
>
> ?
>
> Ralf
>
> -----------------------------------------------------------
>
> )abbrev category CAT Cat
> Cat(S: SetCategory): Category == with
> if S is Integer then foo: () -> Integer

^^^^^^^^^^

This is reccuring trouble: compiler does not support 'is' conditions
in domain/category exports. Unfortunately, trouble is detected
only when you try to use such exports. Actually, this limition
is because compiler has trouble performing some reasonings with
such conditions.

BTW: your code seem to compile fine if I replace 'is Integer'
by 'has IntegerNumberSystem'.

--
Waldek Hebisch