------------------------------------------------------------------------
-- The Agda standard library
--
-- IO only involving infinite objects
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --guardedness #-}
module IO.Infinite where
open import Codata.Musical.Costring using (Costring)
open import Agda.Builtin.String using (String)
open import Data.Unit.Polymorphic.Base using (⊤)
import Data.Unit.Base as Unit0 using (⊤)
open import IO.Base as Base using (IO; lift; lift′)
import IO.Primitive.Core as Prim using (IO; _>>=_; _>>_)
import IO.Primitive.Infinite as Prim
using (getContents; writeFile; appendFile; putStr; putStrLn)
open import Level using (Level; Lift; 0ℓ; suc)
private
variable
a : Level
------------------------------------------------------------------------
-- Simple lazy IO
-- Note that the functions below produce commands which, when
-- executed, may raise exceptions.
-- Note also that the semantics of these functions depends on the
-- version of the Haskell base library. If the version is 4.2.0.0 (or
-- later?), then the functions use the character encoding specified by
-- the locale. For older versions of the library (going back to at
-- least version 3) the functions use ISO-8859-1.
getContents : IO Costring
getContents = lift Prim.getContents
writeFile : String → Costring → IO {a} ⊤
writeFile f s = lift′ (Prim.writeFile f s)
appendFile : String → Costring → IO {a} ⊤
appendFile f s = lift′ (Prim.appendFile f s)
putStr : Costring → IO {a} ⊤
putStr s = lift′ (Prim.putStr s)
putStrLn : Costring → IO {a} ⊤
putStrLn s = lift′ (Prim.putStrLn s)
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