Importing PeanoNat.Nat shadows eq definition

[Villetaneuse]

From Stdlib Require Import PeanoNat.
About eq. (* Corelib.Init.Logiq.eq *)
Import Nat.
About eq. (* Stdlib.Arith.PeanoNat *)

This prevents writing, e.g. eq_refl in a proof term (except for nat of course).

A possible (heavy but maybe beneficial in the long run) fix would be to change Numbers so that equality is Leibniz everywhere instead.
Or I learn to live with it and stop Importing Nat, but this is painful for a (somewhat basic) course.

[SkySkimmer]

Or I learn to live with it and stop Importing Nat, but this is painful for a (somewhat basic) course.

Import Logic after Nat?

[Villetaneuse]

Thank you, it's a good workaround. However, I still think this is a defect in PeanoNat and all Number based modules.

[andres-erbsen]

I agree it's a bad design and should be changed. However, I can't think of an easy immediate fix if you can, I'd consider it very welcome.

In the longer term, I think it would be great to deprecate the Numbers hierarchy and instead bootstrap everything from Z and lia (and/or trocq) like Lean does.