File tree Expand file tree Collapse file tree 2 files changed +8
-0
lines changed Expand file tree Collapse file tree 2 files changed +8
-0
lines changed Original file line number Diff line number Diff line change @@ -562,3 +562,8 @@ Additions to existing modules
562
562
``` agda
563
563
SortingAlgorithm.sort-↭ₛ : ∀ xs → sort xs Setoid.↭ xs
564
564
```
565
+
566
+ * In ` Data.List.Instances ` :
567
+ ``` agda
568
+ instance listIsString : IsString (List Char)
569
+ ```
Original file line number Diff line number Diff line change @@ -16,6 +16,8 @@ import Data.List.Effectful.Transformer as Trans
16
16
using (functor; applicative; monad; monadT)
17
17
open import Data.List.Properties
18
18
using (≡-dec)
19
+ open import Data.List.Literals
20
+ using (isString)
19
21
open import Data.List.Relation.Binary.Pointwise
20
22
using (Pointwise)
21
23
open import Data.List.Relation.Binary.Lex.NonStrict
@@ -42,6 +44,7 @@ instance
42
44
listMonad = monad
43
45
listMonadZero = monadZero
44
46
listMonadPlus = monadPlus
47
+ listIsString = isString
45
48
-- ListT
46
49
listTFunctor = λ {f} {g} {M} {{inst}} → Trans.functor {f} {g} {M} inst
47
50
listTApplicative = λ {f} {g} {M} {{inst}} → Trans.applicative {f} {g} {M} inst
You can’t perform that action at this time.
0 commit comments