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
unpickle function to get the required
I think that's a missing piece indeed...
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
finType. Oh well...
Last updated: Jan 29 2023 at 19:02 UTC