add subst0 to substitute erased equalities in non-erased types

agda · Jan 18, 2024 · cc2a596 · cc2a596
1 parent 984821a
commit cc2a596
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
@@ -124,6 +124,11 @@ lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
 lookup x []              = Nothing
 lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
 
+
+subst0 : (p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
+subst0 p refl z = z
+{-# COMPILE AGDA2HS subst0 transparent #-}
+
 -------------------------------------------------
 -- Unsafe functions