make Z.of_nat not a coercion inside std++

This takes a first step towards #102 by not declaring the coercion in std++. We will add it back in Iris. This can help gauge the fallout of #102, and it would have caught this problem.

mentioned in merge request !254 (merged)

An alternative would be to remove this Coercion entirely from std++. and add it in iris.prelude.prelude.

I would prefer to go all the way immediately, but this could be a sensible stepping stone.

Do we have any idea how much removing the coercion entirely will break in Iris and some major Iris developments (like RustBelt or examples)?

I would prefer to go all the way immediately,

I don't have the time to push that through currently, and would prefer to do it after the deadline.

However, moving the Coercion from here to iris.prelude.prelude should be easy and should still be mostly backwards compatible, so maybe that's better -- it feels a bit less hacky.

Do we have any idea how much removing the coercion entirely will break in Iris and some major Iris developments (like RustBelt or examples)?

No. My guess is "a lot, and fixing is trivial but tedious -- insert these calls everywhere by hand".

Would it make sense to have a shorter name or a notation for this coercion, considering it's likely used often?

mentioned in merge request !259 (merged)

added 7 commits

• f149ab17...2d7f0238 - 6 commits from branch master
• 91fae00c - make Z.of_nat not a coercion inside the prelude implementation

Compare with previous version

resolved all threads

added 1 commit

• 5062a5fc - remove Z.of_nat coercion entirely in std++ (but we'll add it in Iris for now)

Compare with previous version

changed title from make Z.of_nat not a coercion inside the prelude implementation to make Z.of_nat not a coercion inside std++

changed the description

@robbertkrebbers any objections to landing this, and then adding back the coercion in Iris? We can still experiment with notations in separate MRs, if anyone has any good ideas. (Though if you have a good idea we can also try it in this MR.)

resolved all threads

Merging as discussed on Mattermost.

merged

mentioned in commit 3b02de05

@iris-users this is a breaking change if you are using std++ without Iris: Z.of_nat is no longer a coercion. In Iris, we will make it a coercion again, so wherever you import Iris, nothing changes.