Prop-valued classes

Stream: general

[Yaël Dillies]

What is our stance on Prop-valued versions of Type-valued classes? I can find at least three possible instances of such:

• finite instead of docs#fintype
• countable instead of docs#encodable
• docs#order.ideal_Inter_nonempty instead of docs#order_bot (the equivalence between both is not immediate, but you should be able to convince yourself by considering principal ideals)

Of course, if foo is Type-valued, then we can use nonempty foo as the Prop-valued version, but that may become unwiedly?

[Yaël Dillies]

cc @Yury G. Kudryashov

[Kevin Buzzard]

We have docs#is_field but this is to get around some issues with fields having extra uniquely-determined data on top of rings

[Yury G. Kudryashov]

I have a file about countable in a local branch. I'm going to merge master and make it compile by Monday.

[Yury G. Kudryashov]

I pushed branch#YK-countable. It would be nice if someone (@Yaël Dillies ?) adopts this branch. Probably, I won't have time to work on it in the next week or two.