Bill Richter <rich...@math.northwestern.edu>: > Vincent, you gave me a nice exercise which I'll try to work, but it dawned on > me that we can't use that unless we permanently change the parser. E.g. > every time I use miz3, I have to change the parser for that entire HOL Light > session. The same thing goes for your nice hack of quotexpander: it hold for > the entire HOL Light session. Is that right? In that case, I think it would > not be a good idea to install that in HOL Light, I think, as the benefit so > far (improving case & consider a bit) is too low. I think the benefit of > changing the parser permanently would be high enough if we could always infer > the type of a variable in the scope of a variable binding.
Hi Bill, the change is very small actually. The only non backward compatible change is that every usual term starting with ";" (or whatever other symbol that you decide to use) will not be parsed as it would have been before the change. But the chances that a usual HOL term starts with ";" is extremely low (actually I would even not be surprised if it did not parse at all) so you are not losing a lot if any. Now we said that ";" is a bad choice because miz3 already uses it, but many other symbols would have this property, " ' " for instance or the ending " . ". V. ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
