Skip to content

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).