cleanup 'deriving's

cedar-policy · Nov 15, 2023 · 9fdba9c · 9fdba9c
1 parent c121718
commit 9fdba9c
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 6 deletions.
diff --git a/cedar-lean/Cedar/Data/Set.lean b/cedar-lean/Cedar/Data/Set.lean
@@ -30,8 +30,7 @@ namespace Cedar.Data
 
 inductive Set (α : Type u) where
 | mk (l : List α)
-deriving Repr
-deriving instance DecidableEq, Repr, Inhabited, Lean.ToJson for Set
+deriving DecidableEq, Repr, Inhabited, Lean.ToJson
 
 namespace Set
 
@@ -157,4 +156,4 @@ theorem make_eq_if_eqv [LT α] [DecidableLT α] [StrictLT α] (xs ys : List α)
 
 end Set
 
-end Cedar.Data
+end Cedar.Data
diff --git a/cedar-lean/Cedar/Spec/Wildcard.lean b/cedar-lean/Cedar/Spec/Wildcard.lean
@@ -19,9 +19,7 @@ namespace Cedar.Spec
 inductive PatElem where
   | star
   | justChar (c : Char)
-deriving Repr
-deriving instance DecidableEq for PatElem
-deriving instance Inhabited for PatElem
+deriving Repr, DecidableEq, Inhabited
 
 abbrev Pattern := List PatElem