From a5559f9f8e05a8885dc6cc31844ee303fec6f9ae Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com> Date: Tue, 5 Oct 2021 14:13:03 +0200 Subject: [PATCH] fin_sets: add missing Params instance for `set_map` Noticed from VERY slow rewrites. --- theories/fin_sets.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/fin_sets.v b/theories/fin_sets.v index d6c7c31a..9696381f 100644 --- a/theories/fin_sets.v +++ b/theories/fin_sets.v @@ -23,6 +23,7 @@ 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. -- GitLab