Comparing constants
The comparison of constants Constant.compare_const
makes the distinction between structural and semantic comparison. This distinction is not reflected in the way constants are hashed (currently this is done with Hashtbl.hash c
for any constant c
, line 452 in term.ml
). This means that t_hash_generic
cannot be compatible with t_equal_generic
when doing a semantic comparison of constants (optional argument const
set to false
). This can lead to errors, for example when defining a new hash table with these comparison and hash functions.
Also why is semantic comparison not the default for t_equal
? I would expect a call to t_equal
to return true
on two terms that are both printed as 42
.