From 04f48a2bd7442699b7a15fd0e9a771c5a60ba67e Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Fri, 19 Jan 2024 16:38:50 +0100
Subject: [PATCH] Add missing COMPILE pragma for rezz-id

---
 lib/Haskell/Extra/Erase.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lib/Haskell/Extra/Erase.agda b/lib/Haskell/Extra/Erase.agda
index 2e0c9b7c..46d4ef9a 100644
--- 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)