Oh no. So does that mean the import function would have to be updated then. <div class="gmail_quote">On Jul 2, 2015 5:58 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 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>