Hi Brando,
The HOL4 description manual has quite a bit of information, a lot of
which is shared with HOL Light:
http://sourceforge.net/projects/hol/files/hol/kananaskis-13/kananaskis-13-description.pdf/download
I am not sure if there is a similar document for HOL Light.
You can see the HOL Light term structure as it is defined here:
https://github.com/jrh13/hol-light/blob/a1ca1f31539c8e9bd40d324c14951e3c76836787/fusion.ml#L99
Hope this helps!
Regards,
Petros
On 08/11/2019 15:48, Miranda, Brando wrote:
Hi,
This is my first message to the HOL list so hope its not out of the
rules for the list (couldn’t find the rules).
I wanted to find the formal grammar for generating terms (formulas) in
HOL (Light). I was wondering were I could find such a specification?
Thanks!
Brando
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Dr. Petros Papapanagiotou
Chancellor's Fellow in Digital Technologies
CISA, School of Informatics, The University of Edinburgh
Academic Coordinator
IoT Research & Innovation Service
http://homepages.inf.ed.ac.uk/ppapapan/
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
