a custom function
to do the parsing yourself, and that you would have a grammar value embodying
your syntax.
Michael
On 13 Mar 2015, at 10:26 am, Piotr Trojanek piotr.troja...@gmail.com wrote:
Just to close this thread -- I finally got a customized HOL parser by
creating a temporary grammar
calculus
and program semantics, but they heavily depend on their own notation
and I found their reasoning difficult to mechanize in HOL. On the
other extreme, HOL mechanizations of the refinement calculus simply
define the weakest precondition for While as the least fixpoint.
--
Piotr Trojanek
), which
is much less flexible.
--
Piotr Trojanek
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
