erase a in subst0

agda · Jan 23, 2024 · 36a25ff · 36a25ff
1 parent 20e3cbc
commit 36a25ff
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
@@ -101,7 +101,7 @@ errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
 errorWithoutStackTrace {i = ()} err
 
 
-subst0 : (@0 p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
+subst0 : {@0 a : Set} (@0 p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
 subst0 p refl z = z
 {-# COMPILE AGDA2HS subst0 transparent #-}