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

[Robert White]

Sorry I don't know enough about that. I am just a master student. Anyway,
good to hear that. Looking forward to the updates.
On Jul 2, 2015 10:53 PM, "Joe Leslie-Hurd" <joe at gilith.com> wrote:

> Hi Robert,
>
> I'm afraid I may have been confusing. The OpenTheory standard library
> has always had an explicit set type, and will continue to do so
> (knowing what I know now, anyway). So you shouldn't need to change
> anything.
>
> Cheers,
>
> Joe
>
> On Thu, Jul 2, 2015 at 1:50 PM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > 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/20150703/ac8b81cc/attachment.html>