------------------------------------------------------------------------
-- The Agda standard library
--
-- List Literals
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Literals where

open import Agda.Builtin.FromString using (IsString)
open import Data.Unit.Base using (⊤)
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
  }