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.
To define such a constant using 'new_definition' you would have construct the definition term argument, using syntax constructors (such as 'mk_var', 'mk_eq', 'mk_comb', etc). This would mean that terms involving your new constant would get pretty printed as you desire. But you still have the problem that you can't parse in term quotations involving the new constant - they would always require syntax constructors. Mark. on 27/6/12 8:10 AM, Bill Richter <[email protected]> wrote: > .... > > parse_as_infix("seg_less",(12, "right"));; > > let SegmentOrdering_DEF = new_definition > `s seg_less t <=> > ? A B C D X. s = Segment A B /\ t = Segment C D /\ > X IN open (C,D) /\ Segment A B === Segment C X`;; > > .... > > BTW I would have preferred to call it seg<, to go with angle< later, > but HOL Light didn't let me do that. Does anyone know why? ------------------------------------------------------------------------------ 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
