I would try to avoid HOL-Algebra as much as possible. The entire library
is not in a great state and introducing unnecessary dependencies on it
should be avoided.
There is much work to be done there.
Manuel
On 09/04/2019 15:25, Makarius wrote:
> On 09/04/2019 14:06, Manuel Eberl wrote:
>>
On 09/04/2019 14:06, Manuel Eberl wrote:
> Importing Algebra sounds like it would come with various unforeseen
> consequences.
>
> The more modular approach seems more workable to me. I for one think
> that there's no rush; I'd wait until the next release cycle.
I won't participate in this
Importing Algebra sounds like it would come with various unforeseen
consequences.
The more modular approach seems more workable to me. I for one think
that there's no rush; I'd wait until the next release cycle.
Manuel
On 09/04/2019 12:14, Lawrence Paulson wrote:
> I’ve completed porting HOL
I would second this suggestion not to rearrange analysis before the release.
There are mnay users of Analysis but there will only be a few Homology users.
Tobias
On 09/04/2019 12:49, Dr A. Koutsoukou-Argyraki wrote:
why not leave it as a separate Homology library that would be importing both
On 2019-04-09 11:59, Lawrence Paulson wrote:
I’m not sure how to do this without drastically restructuring Analysis.
Maybe we could have separate “top theories” (analogous to Main vs
Complex_Main) within Analysis. But then HOL-Analysis would still
depend on HOL-Algebra.
Or Homology could be a
I’m not sure how to do this without drastically restructuring Analysis.
Maybe we could have separate “top theories” (analogous to Main vs Complex_Main)
within Analysis. But then HOL-Analysis would still depend on HOL-Algebra.
Or Homology could be a new development, importing Analysis, but with
why not leave it as a separate Homology library that would be importing
both Analysis and Algebra for now?
It would then evolve into an Algebraic Topology library with time.
This would also reflect how a "real-life" math library would be
organised.
i.e. : I would prefer your suggestion of
On 09/04/2019 12:14, Lawrence Paulson wrote:
>
> An alternative may be to break up Analysis into several modules, though I
> don’t see how that can be done in time for the next release.
There are approx. 3 weeks left until official Isabelle2019-RC1, so
whatever happens here needs to be finished
