Functions from LabelType to CombinatorialSpecies

Type Constructor

Description

A domain that wraps functions from LabelType to CombinatorialSpecies.

This domain is necessary because of a compiler bug. With the current compiler

: import from List((L: LabelType) -> CombinatorialSpecies L);
S: List((L: LabelType) -> CombinatorialSpecies L) := [];

as used in interpret results in a segfault. The workaround we use here is due to Christian Aistleitner.

ToDo ⊲ 73 ⊳

mrx ⊲ 20 ⊳ 14-Oct-2006: I believe that defining such type might be a good idea anyway, since (L: LabelType) -> CombinatorialSpecies L is used so often. Only the necessity of having to say coerce all the time is a pain. The current name is not so good though, and should be changed.

18-Oct-2006: I tried to replace (L: LabelType) -> CombinatorialSpecies L by LabelSpecies , and F(...)(L:LabelType): CombinatorialSpecies L == add {...} by

: F(...): LabelSpecies == coerce(
(L:LabelType) +-> CombinatorialSpecies L == add {...}
)

but without success. Furthermore, I did not find a solution to the problem of extending List and Set to LabelSpecies . Since the signatures do not match, this cannot be done directly.

452⟨dom: LabelSpecies 452⟩≡   (449)
LabelSpecies: with {
        coerce: ((L: LabelType) -> CombinatorialSpecies L) -> %;
        coerce: % -> ((L: LabelType) -> CombinatorialSpecies L);
#if Axiom
        SetCategory;
#endif
} == add {
        coerce(F: (L: LabelType) -> CombinatorialSpecies L): % == {
                F pretend %
        }
        coerce(F: %): ((L: LabelType) -> CombinatorialSpecies L) == {
                F pretend ((L: LabelType) -> CombinatorialSpecies L)
        }
#if Axiom
        import from List OutputForm;
        coerce(g: %): OutputForm == message("<LabelSpecies>")$OutputForm;
        (x:%) = (y:%):Boolean == false;
#endif
}

Defines:
LabelSpecies, used in chunks 454, 455, 458, 461, 731, and 732.

Uses CombinatorialSpecies 71 and LabelType 62.

16.1 Functions from LabelType to CombinatorialSpecies