Something in std++ enables implicit generalization of instances
The following script fails, as I would expect because k
is not bound:
Class Even (n: nat) := even : exists m, 2 * m = n.
Global Instance even_even: Even (2*k).
However, the following script works:
From stdpp Require Export prelude.
Class Even (n: nat) := even : exists m, 2 * m = n.
Global Instance even_even: Even (2*k).