On 27/06/2012, at 18:21, "Mark" <[email protected]> wrote:
> The name "seg<" is irregular, in that it combines both alpha-numeric and
> symbolic characters. Any names can be used for constants and variables in
> the HOL logic, but HOL Light (and HOL4 I think) have no mechanism for
> *parsing* irregular names. So defining a constant called "seg<" by
> supplying a term quotation won't work.
As it happens HOL4 will parse "irregular names" of the sort you describe. The
trick is to define the underlying constant with a nice name, and to then do
something like
val _ = overload_on ("seg<", ``seglt``)
where seglt is the "nice name". For example, my theory of the lambda calculus
uses -b-> as an infix beta-reduction arrow. With Unicode on, you can get the
same arrow with an inserted Greek beta.
Michael
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
