diff --git a/lib/Haskell/Prim/Applicative.agda b/lib/Haskell/Prim/Applicative.agda index 06d01390..a88a6962 100644 --- 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 index 32edb93a..8024ce07 100644 --- 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