pretty printing displays operators of the same name but different definitions the same

[alleystoughton]

[this was part of another issue, grouping together disparate issues regarding operators and pretty printing]

Here is an example showing how pretty printing can display different operators that have the same name identically, which is confusing. Now clear how to fix this, unless by resorting to printing some operators as non-symbolic ones.

require import AllCore.

op a = 3 < 4.

op (<) (x y : int) = x = y.

print (<).
(*
* In [operators or predicates]:

op (<) (x y : int) : bool = x = y.
abbrev (<)  : real -> real -> bool = lt.
abbrev (<)  : int -> int -> bool = CoreInt.lt.
pred (<) ['a] (p q : 'a -> bool) = p <= q /\ ! q <= p.
*)

lemma foo : a = 3 < 4.
proof.
rewrite /a.
(*
Current goal

Type variables: <none>

------------------------------------------------------------------------
3 < 4 = 3 < 4

- - - -

of course this is really

CoreInt.lt 3 4 = (3 = 4)

and thus not provable, but it seems the first `3 < 4` shouldn't
be displayed this way. *)