Stream: math-comp users

Topic: ✔ rewrite -deprecated_filter_index_enum


view this post on Zulip Pierre Jouvelot (Feb 10 2023 at 22:40):

I proved something like what follows, but what is the best way to avoid using deprecated_filter_index_enum?

Lemma foo (k : 'I_10) : k \in enum 'I_10.
Proof. by rewrite -deprecated_filter_index_enum map_f. Qed.

view this post on Zulip Karl Palmskog (Feb 10 2023 at 23:11):

anything wrong with:

Proof. by rewrite mem_enum. Qed.

view this post on Zulip Pierre Jouvelot (Feb 11 2023 at 07:54):

Thanks. I didn't think about this intermediate rewriting step.

view this post on Zulip Notification Bot (Feb 11 2023 at 07:56):

Pierre Jouvelot has marked this topic as resolved.


Last updated: Jul 25 2024 at 15:02 UTC