Eta-expand definition of pure in Data.Erased in response to agda/agda#4432

jespercockx · gallais · commit 9636263797f5 · 2020-02-25T21:25:40.000Z
diff --git a/src/Data/Erased.agda b/src/Data/Erased.agda
@@ -36,7 +36,7 @@ map : (A → B) → Erased A → Erased B
 map f [ a ] = [ f a ]
 
 pure : A → Erased A
-pure = [_]
+pure x = [ x ]
 
 infixl 4 _<*>_
 _<*>_ : Erased (A → B) → Erased A → Erased B
