nat.subtype.order_iso_of_nat

Stream: general

[Violeta Hernández]

We have docs#nat.subtype.order_iso_of_nat, an order isomorphism between naturals and a decidable subset of naturals. The problem is that it's noncomputable, which given the decidable_rel hypothesis, I assume wasn't the original intention.

[Violeta Hernández]

What should be done here? It probably wouldn't be too hard to code a computable version of this, at the expense of whatever definitional equalities we had going on. Alternatively, we could just remove the decidability hypothesis.

[Eric Rodriguez]

turns out it was originally defined this way (#6113)

[Violeta Hernández]

Oh, that's weird.

[Violeta Hernández]

I'll just remove the assumption: #15190

[Eric Rodriguez]

I do think it'd be easy to code a computable version, but there's no real point, imo