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? <div class="gmail_quote">On Jul 2, 2015 10:29 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, 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>