Indeed, writing Equality.on (nat * nat) will mistakenly interpret * as being the natural number multiplication instead of the cartesian product. The same goes for Build.
We should use the scope given by the type of the argument, and allow manual overriding from the user.
Indeed, writing
Equality.on (nat * nat)will mistakenly interpret*as being the natural number multiplication instead of the cartesian product. The same goes for Build.We should use the scope given by the type of the argument, and allow manual overriding from the user.
Spotted by @ggonthier