------------------------------------------------------------------------
-- The Agda standard library
--
-- String Literals
------------------------------------------------------------------------

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

module Data.String.Literals where

open import Agda.Builtin.FromString using (IsString)
open import Data.Unit.Base using (⊤)
open import Agda.Builtin.String using (String)

isString : IsString String
isString = record
  { Constraint = λ _ → ⊤
  ; fromString = λ s → s
  }