Thank you very much! I confirm your solution works in both HOL K11 and K12.
Chun
> Il giorno 25 mar 2017, alle ore 13:19, Ramana Kumar <ram...@member.fsf.org>
> ha scritto:
>
> OK... You could check directly whether "PAT_X_ASSUM" is bound in the PolyML
> global namespace, and enter it if necessary:
>
> val ns = PolyML.globalNameSpace;
> val () = #enterVal ns ("PAT_X_ASSUM", Option.getOpt (#lookupVal ns
> "PAT_X_ASSUM", Option.valOf(#lookupVal ns "PAT_ASSUM")));
>
> There might be an easier way to conditionally make a declaration that I can't
> think of at the moment. (There's a trickier way using "use"...)
>
> On 25 March 2017 at 21:00, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Hi… thanks, but it doesn’t work in HOL K11 final (where PAT_X_ASSUM is not
> defined):
>
> ---------------------------------------------------------------------
> HOL-4 [Kananaskis 11 (expknl, built Tue Mar 07 09:23:36 2017)]
>
> For introductory HOL help, type: help "hol";
> To exit type <Control>-D
> ---------------------------------------------------------------------
> > val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM;
> poly: : error: Value or constructor (PAT_X_ASSUM) has not been declared
> Found near if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM
> Static Errors
>
> > Il giorno 25 mar 2017, alle ore 04:02, Ramana Kumar <ram...@member.fsf.org>
> > ha scritto:
> >
> > One thing you could try is to use Globals.version, e.g.,
> > val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM;
> >
> > On 25 March 2017 at 07:32, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> > Hi,
> >
> > Currently I’m doing several projects in HOL4, and fortunately Kananaskis-11
> > was finally released early this month, and for now I only use K-11 final
> > release and not chasing and rebuild HOL from Git master any more. On the
> > other side, I finally learnt to use PAT_X_ASSUM to “pop” any assumption I
> > want, just like a more flexible version of POP_ASSUM.
> >
> > My goal is to have my proof scripts being able to run in both K11 final
> > release and current ongoing K12 versions, so when I need to “pop” an
> > assumption, I always write it as PAT_X_ASSUM and having this line in all my
> > *Script.sml files:
> >
> > (* This is for Kananaskis 11 only, remove it for K12. *)
> > val PAT_X_ASSUM = PAT_ASSUM;
> >
> > The question is, at PolyML (and MosML) level, how to write code to
> > re-define PAT_X_ASSUM only in K11 final release (and before)? Or there’s
> > another better solution to this entire problem?
> >
> > Regards,
> >
> > Chun Tian
> >
> >
> > ------------------------------------------------------------------------------
> > Check out the vibrant tech community on one of the world's most
> > engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
>
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
