[isabelle-dev] cardinality primitives in Isabelle/HOL?

[Andrei Popescu]

 Dear Larry, dear all,


>> 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.


Sorry for my late reply. I agree it makes sense to move such basic operators (and facts) into Main. The Ordinals and Cardinals development was "destined" to this sort of exports from the very beginning.


Best wishes,


Andrei


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

Message: 1
Date: Wed, 23 Jan 2019 14:33:30 +0000
From: Lawrence Paulson <lp15 at cam.ac.uk>
To: Jasmin Blanchette <j.c.blanchette at vu.nl>
Cc: Traytel Dmitriy <traytel at inf.ethz.ch>, isabelle-dev
        <isabelle-dev at in.tum.de>
Subject: Re: [isabelle-dev] [Spam]  cardinality primitives in
        Isabelle/HOL?
Message-ID: <CB1B1CE8-3491-4FCE-8494-6D2E3E68BB94 at cam.ac.uk>
Content-Type: text/plain;       charset=utf-8

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. <j.c.blanchette at vu.nl> wrote:
>
> 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 some cardinality material. When we moved the BNF package into Main, I surgically split the HOL-Cardinals theories into two, moving the exact dependencies into Main and leaving the rest outside. As a result, it's pretty random what's in Main and what's outside. The alternative -- moving all of HOL-Cardinals into Main -- seemed undesirable because it would slow down building Main quite a bit.
>
> Jasmin
>



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190126/24621596/attachment-0002.html>