A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://agda.github.io/agda-stdlib/master/Codata.Musical.Costring.html below:

Codata.Musical.Costring

Codata.Musical.Costring
------------------------------------------------------------------------
-- 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

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4