Applying suggestions

agda · Mar 1, 2024 · bb89fd2 · bb89fd2
1 parent 6959429
commit bb89fd2
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 9 deletions.
diff --git a/lib/Haskell/Prim/Applicative.agda b/lib/Haskell/Prim/Applicative.agda
@@ -16,9 +16,7 @@ open import Haskell.Prim.Tuple
 
 -- ** base
 record Applicative (f : Set → Set) : Set₁ where
-  infixl 4 _<*>_
-  infixl 4 _<*_
-  infixl 4 _*>_
+  infixl 4 _<*>_ _<*_ _*>_
   field
     pure  : a → f a
     _<*>_ : f (a → b) → f a → f b
@@ -28,9 +26,7 @@ record Applicative (f : Set → Set) : Set₁ where
 -- ** defaults
 record DefaultApplicative (f : Set → Set) : Set₁ where
   constructor mk
-  infixl 4 _<*>_
-  infixl 4 _<*_
-  infixl 4 _*>_
+  infixl 4 _<*>_ _<*_ _*>_
   field
     pure  : a → f a
     _<*>_ : f (a → b) → f a → f b

diff --git a/lib/Haskell/Prim/String.agda b/lib/Haskell/Prim/String.agda
@@ -7,10 +7,10 @@ open import Haskell.Prim.Foldable
 
 --------------------------------------------------
 -- String
--- This is _not_ the builtin String type of Agda;
+-- This is _not_ the builtin String type of Agda
 -- which is defined by postulates.
--- fromString can be used to produce Haskell strings
--- from that.
+-- `fromString` can be used to convert back
+-- to builtin Agda strings.
 
 String = List Char