Christian Doczkal (Jan 29 2021 at 17:24): 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?
Cyril Cohen (Jan 29 2021 at 17:37):I think that's a missing piece indeed...
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