Seems a good idea to me. Given ETA_AX, it's easy to show equivalence with current HOL Light, and it's always better to have closed formulae coming out of definition commands.
One small point: the formulae as written in the linked message do not have the intended syntactic form (due to bracketing), and should of course be written as this: (\a. abs (rep a)) = \a. a P = (\r. rep (abs r) = r) Mark. on 16/10/14 5:19 PM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote: > Hi all, > > There has been an interesting discussion on the OpenTheory mailing list > recently regarding how to simplify the two theorems produced by a type > definition in HOL Light and remove their free variables. The latest message > in the thread, which shows the suggestions by Mario Carneiro can be found > here: > http://www.gilith.com/pipermail/opentheory-users/2014-October/000415.html. > > I'm cross-posting to this list because I think using Mario's suggestions > would be an improvement to both HOL Light and Opentheory. I hope the > respective authors of those systems might agree and implement the changes, > and that anyone else with an interest might voice their opinion. > > Cheers, > Ramana > > > > ---------------------------------------- > > ---------------------------------------------------------------------------- > -- > Comprehensive Server Monitoring with Site24x7. > Monitor 10 servers for $9/Month. > Get alerted through email, SMS, voice calls or mobile push notifications. > Take corrective actions from your mobile device. > http://p.sf.net/sfu/Zoho > > > ---------------------------------------- > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------------------------ Comprehensive Server Monitoring with Site24x7. Monitor 10 servers for $9/Month. Get alerted through email, SMS, voice calls or mobile push notifications. Take corrective actions from your mobile device. http://p.sf.net/sfu/Zoho _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
