Erase arguments a and x of rezzErase

agda · Dec 22, 2023 · 07c9d3d · 07c9d3d
1 parent bda9466
commit 07c9d3d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/Haskell/Extra/Erase.agda b/lib/Haskell/Extra/Erase.agda
@@ -69,7 +69,7 @@ module Haskell.Extra.Erase where
                    ne = subst NonEmpty (sym p) itsNonEmpty
   {-# COMPILE AGDA2HS rezzTail inline #-}
 
-  rezzErase : Rezz (Erase a) (Erased x)
+  rezzErase : {@0 a : Set} {@0 x : a} → Rezz (Erase a) (Erased x)
   rezzErase {x = x} = Rezzed (Erased x) refl
   {-# COMPILE AGDA2HS rezzErase inline #-}