[ re agda#357 ] Wrap result of guard in Erase

jespercockx · Sep 12, 2024 · 1f9ade6 · 1f9ade6
1 parent ffae44a
commit 1f9ade6
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/lib/Haskell/Control/Monad.agda b/lib/Haskell/Control/Monad.agda
@@ -4,7 +4,8 @@ open import Haskell.Prim
 open import Haskell.Prim.Bool
 open import Haskell.Prim.Monad
 open import Haskell.Prim.String
+open import Haskell.Extra.Erase
 
-guard : {{ MonadFail m }} → (b : Bool) → m (b ≡ True)
-guard True = return refl
+guard : {{ MonadFail m }} → (b : Bool) → m (Erase (b ≡ True))
+guard True = return (Erased refl)
 guard False = fail "Guard was not True"