Every term in HOL can be summarised by the BNF
term ::= var | const | term @ term | \v. term
where @ is function application (and if you use concrete syntax, you don’t
write the @), and \v. term represents a lambda-abstraction. If you want to
programmatically generate terms, using this view
The Twelfth NASA Formal Methods Symposium
https://ti.arc.nasa.gov/events/nfm-2020/
11 - 15 May 2020
NASA Ames Research Center, Moffett Field, CA, USA
Th
And for HOL Zero there is Appendix C of the User Manual that gives a
formal grammar of the HOL Zero concrete syntax. Again, this is fairly
similar to HOL Light's and HOL4's, but there are numerous small
differences. Note that the formal grammar hasn't actually been checked
(as far as I'm awar
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 Li
