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 <l...@cam.ac.uk>
To: Jasmin Blanchette <j.c.blanche...@vu.nl>
Cc: Traytel Dmitriy <tray...@inf.ethz.ch>, isabelle-dev
<isabelle-...@in.tum.de>
Subject: Re: [isabelle-dev] [Spam] cardinality primitives in
Isabelle/HOL?
Message-ID: <cb1b1ce8-3491-4fce-8494-6d2e3e68b...@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.blanche...@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
>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
