decode vs decode2

Stream: general

[Yaël Dillies]

In data/equiv/encodable/basic, decode : ℕ → option α is required to be a partial inverse to encode : α → ℕ, but is still allowed to return some a outside of the range of encode. To prevent that, we define decode2 to be decode on set.range encode and none elsewhere.
In practice, it seems that decode2 is the function that actually gets used, as it is better behaved. What do people think of renaming decode to decode' and decode2 to decode? This could go along with restating some lemmas that are currently about decode.

[Yaël Dillies]

Actually, I'm not sure anymore it's such a good idea.