In HOL4, all code is passed through a "quotation filter" which does roughly
the following transformations:
`x y z ^(a b c) w` = [QUOTE "x y z ", ANTIQUOTE (a b c), QUOTE " w"]
``foo`` = Term`foo` = Term[...]
``:bar`` = Type`bar` = Type[...]
Term has type term frag list -> term.
Type has type ho
Thanks, Ramana! You're the person I wanted to talk to. I already had a vague
understand of what you explained (thanks for explaning), but I have a different
question about HOL4:
I'm convinced that the solution to my problem involves camlp (I use
camlp5-6.05), as I can't find anything in the HO
Hi Bill,
Short answer: string_of_term
Long answer:
let me try to make things clearer about what happens in HOL-Light
(pretty similar, conceptually, to what happens in HOL4) when you type in
something like `bla`:
1. the quotation `bla` is turned (by camlp5 indeed) into an expression
of type pre
