add a function to obtain a set with all elements of a finite type
Merged
add a function to obtain a set with all elements of a finite type
ralf/fin_to_set
into
master
2 unresolved threads
2 unresolved threads
This lets us use the existing nice gmap
/gset
infrastructure even for total functions when the domain type is finite.
Edited by Ralf Jung
Merge request reports
Activity
Filter activity
added 1 commit
- 1f024e52 - add a way to obtain a set with all elements of a finite type
- Resolved by Ralf Jung
mentioned in commit dff135cd
873 873 Proof. induction 1; set_solver. Qed. 874 874 End option_and_list_to_set. 875 875 876 (** * Finite types to sets. *) 877 Definition fin_to_set (A : Type) `{SemiSet A C, Finite A} : C := 873 873 Proof. induction 1; set_solver. Qed. 874 874 End option_and_list_to_set. 875 875 876 (** * Finite types to sets. *) 877 Definition fin_to_set (A : Type) `{SemiSet A C, Finite A} : C := 878 list_to_set (enum A). 879 880 Section fin_to_set. 881 Context `{SemiSet A C, Finite A}. 882 Implicit Types a : A. 883 884 Lemma elem_of_fin_to_set a : a ∈ fin_to_set A. RE 39713291
SemiSet
does not have aHint Mode
, hence this works without type annotation. If you implement my suggestion above, this should fail, even with newer Coq versions, without type annotation.That said, we probably should also give classes like
SemiSet
aHint Mode
.
Please register or sign in to reply