HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Implement variable sets

Open ordinarymath opened this issue 4 months ago • 1 comments

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.

ordinarymath avatar Sep 06 '25 05:09 ordinarymath

Bonus points implement a way to get a unique name in linear time. This can be done using the fact that a << a ^ "'"

ordinarymath avatar Sep 06 '25 05:09 ordinarymath