Stream: math-comp users

Topic: obtaining countability from finiteness


view this post on Zulip Christian Doczkal (Jan 29 2021 at 17:24):

Assuming I have some T : eqType together with a proof of Finite.axiom Ts for some Ts : seq T. Is there a direct way of turning T into a finite type, that does not involve explicitly mentioning any pickle/unpickle function to get the required countType instance?

view this post on Zulip Cyril Cohen (Jan 29 2021 at 17:37):

I think that's a missing piece indeed...

view this post on Zulip Christian Doczkal (Jan 29 2021 at 19:13):

Okay, in my case, Ts is actually a concrete nonempty list enumerating an inductive without parameters , so I can do:

Lemma foo: cancel (index^~ Ts) (nth t0 Ts). Proof. by case. Qed.

followed by the usual litany of instances for countType, choiceType, and finType. Oh well...


Last updated: Jan 29 2023 at 19:02 UTC