    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Costrings
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --guardedness #-}

    module Codata.Musical.Costring where

    open import Codata.Musical.Colist.Base as Colist using (Colist)
    open import Data.Char.Base using (Char)
    open import Data.String.Base as String using (String)
    open import Function.Base using (_∘_)

    -- Possibly infinite strings.

    Costring : Set
    Costring = Colist Char

    -- Methods

    toCostring : String → Costring
    toCostring = Colist.fromList ∘ String.toList