move subst0 to Law.Equality

agda · Jan 23, 2024 · a618fac · a618fac
1 parent 36a25ff
commit a618fac
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 5 deletions.
diff --git a/lib/Haskell/Law/Equality.agda b/lib/Haskell/Law/Equality.agda
@@ -57,3 +57,11 @@ _∎ _ = refl
 
 syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
 syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z
+
+
+-------------------------------------------------
+-- Utility Functions
+
+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 #-}
diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
@@ -100,11 +100,6 @@ error {i = ()} err
 errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
 errorWithoutStackTrace {i = ()} err
 
-
-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 #-}
-
 -------------------------------------------------
 -- More List functions
 --   These uses Eq, Ord, or Foldable, so can't go in Prim.List without