Thanks, Vince! That's great we're in agreement about the same symbol being given two different types. How hard would it be to change HOL Light so that it behaves like Coq:
Note that having an environment (i.e., a mapping from variable names to types) is what is done in Coq for instance. It's a simple question I'm asking here: HOL Light does a lot less than you think: it just sees a variable with name "v" and type "real^2", now if it sees elsewhere a variables with the same name and same type then they are equal. As simple as that. How does HOL Light manage to see the earlier variable with name "v" and type "real^2"? I would think it would be because of an environment, but you tell me that's not true. Where would these environments live in the implementation of the logic? Ramana, all I know is that 1) retypecheck takes an environment as its first argument, and the environment has type (string * pretype) list 2) Freek's miz3.ml and John's mizar.ml are the only places in the HOL Light sources where retypecheck is given a non-empty environment as an argument. I figure it can't be that hard to understand what they did, especially if we use strings, as I posted here recently, instead of preterms. -- Best, Bill ------------------------------------------------------------------------------ Try New Relic Now & We'll Send You this Cool Shirt New Relic is the only SaaS-based application performance monitoring service that delivers powerful full stack analytics. Optimize and monitor your browser, app, & servers with just a few lines of code. Try New Relic and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
