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

[Robert White]

The HOL light fork and Holide? Or maybe I dont need to worry about it as
long as you don't change the article files?
On Jul 2, 2015 10:29 PM, "Joe Leslie-Hurd" <joe at gilith.com> wrote:

> Hi Robert,
>
> That depends - into which system are you planning on importing
> OpenTheory theories?
>
> Cheers,
>
> Joe
>
> On Thu, Jul 2, 2015 at 9:39 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > 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/284b23ec/attachment-0001.html>