------------------------------------------------------------------------
-- The Agda standard library
--
-- IO handles: simple bindings to Haskell types and functions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --guardedness #-}
module IO.Handle where
open import Level using (Level)
open import Data.Unit.Polymorphic.Base using (⊤)
open import IO.Base using (IO; lift; lift′)
private variable a : Level
------------------------------------------------------------------------
-- Re-exporting types and constructors
open import IO.Primitive.Handle as Prim public
using ( BufferMode
; noBuffering
; lineBuffering
; blockBuffering
; Handle
; stdin
; stdout
; stderr
)
------------------------------------------------------------------------
-- Wrapping functions
hSetBuffering : Handle → BufferMode → IO {a} ⊤
hSetBuffering hdl bm = lift′ (Prim.hSetBuffering hdl bm)
hGetBuffering : Handle → IO BufferMode
hGetBuffering hdl = lift (Prim.hGetBuffering hdl)
hFlush : Handle → IO {a} ⊤
hFlush hdl = lift′ (Prim.hFlush hdl)
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