Thanks, Rob! This is helpful info:
In all the HOLs, you will find that the parser uses various
constants like [the SETSPEC definition] to represent derived
syntactic constructs (like set comprehensions) in terms of
primitive constructs (like conjunction and equality) in such a way
that the pretty-printer can recover the structure of the derived
construct from the primitive syntax.
This won't help me understand parser.ml, but I it will help me understand
sets.ml. I tried your dest_comb and dest_abs tricks on your original example:
# `{y | y > 6}`;;
val it : term = `{y | y > 6}`
# dest_comb it;;
val it : term * term =
(`GSPEC`, `\GEN%PVAR%218. ?y. SETSPEC GEN%PVAR%218 (y > 6) y`)
# dest_abs it;;
Error: This expression has type term * term
but an expression was expected of type term = Hol.term
I tried something like this when you first posted, but I didn't think to use
dest_comb. Do you have any general tips on how to recognize a term as say a
combination (which worked here) on an abstraction (not here)?
--
Best,
Bill
------------------------------------------------------------------------------
Rapidly troubleshoot problems before they affect your business. Most IT
organizations don't have a clear picture of how application performance
affects their revenue. With AppDynamics, you get 100% visibility into your
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
