Sorry I don't know enough about that. I am just a master student. Anyway, good to hear that. Looking forward to the updates. <div class="gmail_quote">On Jul 2, 2015 10:53 PM, "Joe Leslie-Hurd" <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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 <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> 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" <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> 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" <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 >> >> <<a href="mailto:Michael.Norrish@nicta.com.au">Michael.Norrish@nicta.com.au</a>> wrote: >> >> > >> >> >> On 2 Jul 2015, at 06:57, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 >> >> > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >> >> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </blockquote></div>