search

mattam82 / Coq-Equations

A function definition package for Coq
http://mattam82.github.io/Coq-Equations
GNU Lesser General Public License v2.1
223 stars 44 forks source link

Warning for inlining Signature for #622

Open thomas-lamiaux opened 4 weeks ago

thomas-lamiaux commented 4 weeks ago

A warning

Automatically inlined signature for type vec. Use [Derive Signature for vec.] to avoid this.

Is triggered when deriving NoConfusionHom but not when deriving NoConfusion. I would have expected the opposite.

Further, is there even a need for a warning ? I would expect users not to have to derive Signature as it exposes the internal interface which users should not have to care about ?

TheoWinterhalter commented 4 weeks ago

Well if it inlines it, then it might end up doing so several time, which would be inefficient I think. Hence why it asks the user to derive the signature once and for all? If it could be a quickfix then all would be good no?

thomas-lamiaux commented 4 weeks ago

That could work, but why can't Derive NoConfusion = Derive NoConfusion + Signature ? (you only need to derive it once, right ?)

TheoWinterhalter commented 4 weeks ago

My guess would be that this way you know that this is a side effect of NoConfusion so that you don't also Derive Signature later. It becomes a bit more predictable what is happening and when.

thomas-lamiaux commented 4 weeks ago

It but my point is should the user be allowed to derive signature at all ? Shouldn't it be done automatically ?