Work around for agda/agda2hs#346

jespercockx · Jul 27, 2024 · 11bbc77 · 11bbc77
1 parent 42832b0
commit 11bbc77
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/src/Agda/Core/Conversion.agda b/src/Agda/Core/Conversion.agda
@@ -42,12 +42,6 @@ data ConvBranches {@0 α} : @0 Branches α cs → @0 Branches α cs → Set wher
                 → ConvBranches bs1 bs2
                 → ConvBranches (BsCons b1 bs1) (BsCons b2 bs2)
 
-
-{-# COMPILE AGDA2HS Conv     #-}
-{-# COMPILE AGDA2HS ConvBranch #-}
-{-# COMPILE AGDA2HS ConvBranches #-}
-{-# COMPILE AGDA2HS ConvSubst #-}
-
 infix 3 Conv
 syntax Conv x y        = x ≅ y
 syntax ConvSubst us vs = us ⇔ vs
@@ -117,3 +111,9 @@ data ConvSubst {α} where
          → u ≅ v
          → us ⇔ vs
          → (SCons {x = x} u us) ⇔ (SCons {x = x} v vs)
+
+-- These have to be here, see https://github.com/agda/agda2hs/issues/346
+{-# COMPILE AGDA2HS Conv     #-}
+{-# COMPILE AGDA2HS ConvBranch #-}
+{-# COMPILE AGDA2HS ConvBranches #-}
+{-# COMPILE AGDA2HS ConvSubst #-}