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

Merge branch 'finite_sets' into 'master'

fin_sets: add missing Params instance for `set_map`

See merge request iris/stdpp!328
parents a00c96c5 a5559f9f
No related branches found
No related tags found
1 merge request!328fin_sets: add missing Params instance for `set_map`
Pipeline #54757 passed
......@@ -23,10 +23,11 @@ Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
(f : A B) (X : C) : D :=
list_to_set (f <$> elements X).
Typeclasses Opaque set_map.
Global Instance: Params (@set_map) 8 := {}.
Global Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
fresh elements.
Typeclasses Opaque set_filter.
Typeclasses Opaque set_fresh.
(** We generalize the [fresh] operation on sets to generate lists of fresh
elements w.r.t. a set [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