From 2dcb8551a3bb266530785fb770882ec4bd415450 Mon Sep 17 00:00:00 2001 From: rvs314 Date: Mon, 30 Jun 2025 18:22:35 -0400 Subject: [PATCH 1/4] Add instances of `IsString (List Char)` --- src/Data/List/Instances.agda | 3 +++ src/Data/List/Literals.agda | 11 ++++++----- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/Data/List/Instances.agda b/src/Data/List/Instances.agda index 2f5be06a75..d239be7eee 100644 --- a/src/Data/List/Instances.agda +++ b/src/Data/List/Instances.agda @@ -16,6 +16,8 @@ import Data.List.Effectful.Transformer as Trans using (functor; applicative; monad; monadT) open import Data.List.Properties using (≡-dec) +open import Data.List.Literals + using (isString) open import Data.List.Relation.Binary.Pointwise using (Pointwise) open import Data.List.Relation.Binary.Lex.NonStrict @@ -42,6 +44,7 @@ instance listMonad = monad listMonadZero = monadZero listMonadPlus = monadPlus + listIsString = isString -- ListT listTFunctor = λ {f} {g} {M} {{inst}} → Trans.functor {f} {g} {M} inst listTApplicative = λ {f} {g} {M} {{inst}} → Trans.applicative {f} {g} {M} inst diff --git a/src/Data/List/Literals.agda b/src/Data/List/Literals.agda index 80d57901d1..ad098cf36d 100644 --- a/src/Data/List/Literals.agda +++ b/src/Data/List/Literals.agda @@ -14,8 +14,9 @@ open import Agda.Builtin.Char using (Char) open import Agda.Builtin.List using (List) open import Data.String.Base using (toList) -isString : IsString (List Char) -isString = record - { Constraint = λ _ → ⊤ - ; fromString = λ s → toList s - } +instance + isString : IsString (List Char) + isString = record + { Constraint = λ _ → ⊤ + ; fromString = λ s → toList s + } From a0416cfaf2b3a95634609e101893ead3605d115a Mon Sep 17 00:00:00 2001 From: rvs314 Date: Tue, 1 Jul 2025 16:41:21 -0400 Subject: [PATCH 2/4] Don't also `isString` as an instance from `Data.List.Literals` --- src/Data/List/Literals.agda | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Data/List/Literals.agda b/src/Data/List/Literals.agda index ad098cf36d..80d57901d1 100644 --- a/src/Data/List/Literals.agda +++ b/src/Data/List/Literals.agda @@ -14,9 +14,8 @@ open import Agda.Builtin.Char using (Char) open import Agda.Builtin.List using (List) open import Data.String.Base using (toList) -instance - isString : IsString (List Char) - isString = record - { Constraint = λ _ → ⊤ - ; fromString = λ s → toList s - } +isString : IsString (List Char) +isString = record + { Constraint = λ _ → ⊤ + ; fromString = λ s → toList s + } From 80a997949aed57b69dc7b5b46503b59e505509b2 Mon Sep 17 00:00:00 2001 From: rvs314 Date: Tue, 1 Jul 2025 16:42:23 -0400 Subject: [PATCH 3/4] Add changelog entry --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4adf540ce4..30457d8c20 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -443,3 +443,8 @@ Additions to existing modules ```agda map⁻ : Unique (map f xs) → Unique xs ``` + +* In `Data.List.Instances`: + ```agda + instance listIsString : IsString (List Char) + ``` From 0c059a78fce392bb3c36f4770fb4c2f7543354d0 Mon Sep 17 00:00:00 2001 From: rvs314 Date: Wed, 2 Jul 2025 17:07:06 -0400 Subject: [PATCH 4/4] Whitespace fix --- CHANGELOG.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index cc12faa6cf..bdd1a7c0a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -499,7 +499,8 @@ Additions to existing modules ```agda SortingAlgorithm.sort-↭ₛ : ∀ xs → sort xs Setoid.↭ xs ``` - + * In `Data.List.Instances`: ```agda - instance listIsString : IsString (List Char) \ No newline at end of file + instance listIsString : IsString (List Char) + ```