Add missing COMPILE pragma for rezz-id

agda · Jan 19, 2024 · 04f48a2 · 04f48a2
1 parent f37dff8
commit 04f48a2
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/lib/Haskell/Extra/Erase.agda b/lib/Haskell/Extra/Erase.agda
@@ -42,6 +42,7 @@ module Haskell.Extra.Erase where
   instance
     rezz-id : {x : a} → Rezz a x
     rezz-id = rezz _
+  {-# COMPILE AGDA2HS rezz-id inline #-}
 
   rezzCong : {@0 a : Set} {@0 x : a} (f : a → b) → Rezz a x → Rezz b (f x)
   rezzCong f (Rezzed x p) = Rezzed (f x) (cong f p)