Re: [isabelle] lexical matters
on 18/1/11 7:10 PM, Makarius <makarius at sketis.net> wrote:
> Dvid Matthews kindly provides ways in Poly/ML to manage the whole
> compilation process in user space, including printing and binding of the
> results. One would merely have to protect agains shadowing of certain
> structure names, say.
Oh good. This is excellent news. How long has this been available for?
A related problem is overwriting a datatype's pretty printer. Do you know
if Poly/ML can protect against this?
> When you've showed me an early version of HOL0 in Cambridge ITP 2009, I
> have already pointed out that OCaml is not the best platform for that (due
> to its mutable strings and silently overflowing machine words called
Yes you did (was it Montreal ITP 2008?). HOL Zero uses a technique to avoid
problems with mutable strings (unlike HOL Light) and doesn't use machine
words for its representation of natural number numerals (like HOL Light).
But you are right - OCaml is not the best language. Larry convinced me a
few months ago that SML is simply more well-defined. I plan to port it to
SML as a priority as soon version 1.0 is out. But this port might not be
until next year.
This archive was generated by a fusion of
Pipermail (Mailman edition) and