[opentheory-users] error loading article files (again?).

[Robert White]

Oh no. So does that mean the import function would have to be updated then.
On Jul 2, 2015 5:58 PM, "Joe Leslie-Hurd" <joe at gilith.com> wrote:

> Hi Michael,
>
> I think your statement is correct, because both HOL Light and HOL4 use
> predicates rather than an explicit set type, so if OpenTheory also
> used predicates it would simplify translation between these two
> environments. And indeed, it complicates export if an explicit set
> type has to be reconstructed from predicates.
>
> However, one design principle of OpenTheory is that whenever there is
> a trade-off between simplifying import or export then it's better to
> simplify importing, and in this case it's easy to drop the explicit
> set type in favour of predicates during import.
>
> And there are other environments that do implement explicit set types,
> such as Haskell. When exporting theories as Haskell packages I want to
> export explicit sets as Haskell sets, which would be difficult if
> OpenTheory used predicates.
>
> Cheers,
>
> Joe
>
> On Wed, Jul 1, 2015 at 10:38 PM, Michael Norrish
> <Michael.Norrish at nicta.com.au> wrote:
> >
> >> On 2 Jul 2015, at 06:57, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >
> >> However, I can answer your question right now. I do want the
> >> OpenTheory fork of HOL Light to be as close as possible to the main
> >> trunk of HOL Light, but there are certain changes that are required to
> >> export a standard theory library (which is the primary purpose of this
> >> fork). For example, introducing an explicit set type (A set) rather
> >> than the predicate (A -> bool) and removing default cases (e.g., PRE 0
> >> = 0) are necessary to ensure the standard theory library can be used
> >> in as many environments as possible.
> >
> > Is it not now our experience that providing an explicit set type
> actually makes it *harder* to use OpenTheory in both HOL4 and HOL Light?
> >
> > Michael
> >
> > ________________________________
> >
> > The information in this e-mail may be confidential and subject to legal
> professional privilege and/or copyright. National ICT Australia Limited
> accepts no liability for any damage caused by this email or its attachments.
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150702/f19e111e/attachment.html>