This makes perfect sense to me.
I suggest moving at least the definition of Fpow into Main (it’s small, and
fundamental) while creating a new Library entry for my own new material.
Larry
> On 23 Jan 2019, at 12:48, Blanchette, J.C. wrote:
>
> Hi Larry,
>
> You wrote:
>
>> The theorem
Hi Larry,
You wrote:
> The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so
> clearly a lot of facts about cardinals are available already in Main.
FYI: As you might already know or deduced from the name convention, the
(co)datatype (a.k.a. "BNF") package is based on
