Skip to content

Instantly share code, notes, and snippets.

@puffnfresh

puffnfresh/Main.agda

Last active July 30, 2017 01:59
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save puffnfresh/0def5a2c09d7da144c0d7018b88bcfc2 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save puffnfresh/0def5a2c09d7da144c0d7018b88bcfc2 to your computer and use it in GitHub Desktop.
Download ZIP
cat in Agda
Raw
Main.agda
module Main where
import IO.Primitive as Prim
open import Coinduction
open import Data.BoundedVec.Inefficient using (toList)
open import Data.Colist using (take)
open import Data.Nat
open import Data.String using (Costring; String; fromList)
open import Data.Unit
open import IO
costringToString : ℕ → Costring → String
costringToString n c = fromList (toList (take n c))
cat : IO ⊤
cat = ♯ getContents >>= (\cs → ♯ (putStrLn (costringToString 2048 cs)))
main : Prim.IO ⊤
main = run cat
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment