Skip to content
Snippets Groups Projects
Commit e9aae334 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'finite_sets_2' into 'master'

Mark set_size and set_fold as TC opaque

See merge request iris/stdpp!329
parents fce3654d e3157145
No related branches found
No related tags found
No related merge requests found
...@@ -10,9 +10,11 @@ Set Default Proof Using "Type*". ...@@ -10,9 +10,11 @@ Set Default Proof Using "Type*".
(** Operations *) (** Operations *)
Global Instance set_size `{Elements A C} : Size C := length elements. Global Instance set_size `{Elements A C} : Size C := length elements.
Typeclasses Opaque set_size.
Definition set_fold `{Elements A C} {B} Definition set_fold `{Elements A C} {B}
(f : A B B) (b : B) : C B := foldr f b elements. (f : A B B) (b : B) : C B := foldr f b elements.
Typeclasses Opaque set_fold.
Global Instance set_filter Global Instance set_filter
`{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X, `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment