Printing type parameters of constants #457
Description
Consider the following example:
require import AllCore.
op card ['a] : int. (* Would have an actual definition, of course *)
lemma test: card<:bool> = 2.
The current goal is now card = 2. In the present situation, it is obvious that this means card<:bool> = 2. However, in more complex situations, the type are not obvious (e.g., when card = ... is in a subgoal generated by some tactic, or after rewriting glob-types). See for example the code in #451.
It would be great to have some way to show those type annotations, i.e., show card<:bool> = 2. Either a pragma that shows them all or something clever that shows the ones that aren't obvious.