HOL
HOL copied to clipboard
Implement variable sets
Right now there's a lot wasted time in code that gets the free variables of a term where Term.compare is called. This requires two checks whether the term had the Fv constructor before the terms are actually being compared. var_compare doesn't help as the checks still need to be done. I'm not sure whether the data stored should be string or string * type might need. Strings are useful for computing variants but there might be other code that only care about unique names with respect to a type.
Bonus points implement a way to get a unique name in linear time. This can be done using the fact that a << a ^ "'"