The second restriction is more severe. In fact, I think it's a show
stopper. The current signature of Plus is
Plus(
F: (T: LabelType) -> CombinatorialSpecies(T),
G: (T: LabelType) -> CombinatorialSpecies(T)
)(L: LabelType): CombinatorialSpecies(L) == add { ... }
Although this compiles and loads well, we get
)sh Plus
Plus(F: (LabelType -> CombinatorialSpecies T),G: (LabelType ->
CombinatorialSpecies T)) is a domain constructor
Abbreviation for Plus is PLUS
This constructor is exposed in this frame.
Issue )edit species.as to see algebra source code for PLUS
------------------------------- Operations --------------------------------
Plus(F,G) is a domain constructor.
Abbreviation for Plus is PLUS
This constructor is exposed in this frame.
Issue )edit species.as to see algebra source code for PLUS
------------------------------- Operations --------------------------------
That's it. In fact, we cannot even really try to use it:
(5) -> Plus(SingletonSpecies, SingletonSpecies) IntegerLabel
Although SingletonSpecies is the name of a constructor, a full type
must be specified in the context you have used it. Issue )show
SingletonSpecies for more information.
depressing.