Commit 2021-09-08 06:17 189fe5bd

feat(data/nat/enat): refactor coe from nat to enat (#9023) The coercion from nat to enat was defined to be enat.some. But another coercion could be inferred from the additive structure on enat, leading to confusing goals of the form ↑n = ↑n where the two sides were not defeq. We now make the coercion inferred from the additive structure the default, even though it is not computable. A dedicated function enat.some is introduced, to be used whenever computability is important.