[ re #357 ] Erase type arguments of mapDec

The types a and b do not appear in Haskell code, so they should be marked as erased
agda · Sep 24, 2024 · 8073476 · 8073476
1 parent aafa987
commit 8073476
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/lib/Haskell/Extra/Dec.agda b/lib/Haskell/Extra/Dec.agda
@@ -35,7 +35,8 @@ Dec : ∀ {ℓ} → @0 Set ℓ → Set ℓ
 Dec P = ∃ Bool (Reflects P)
 {-# COMPILE AGDA2HS Dec inline #-}
 
-mapDec : @0 (a → b)
+mapDec : {@0 a b : Set}
+       → @0 (a → b)
        → @0 (b → a)
        → Dec a → Dec b
 mapDec f g (True  ⟨ x ⟩) = True  ⟨ f x   ⟩