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

Revisions

  1. puffnfresh revised this gist Dec 7, 2016. No changes.
  2. puffnfresh revised this gist Dec 7, 2016. 1 changed file with 1 addition and 8 deletions.
    9 changes: 1 addition & 8 deletions Main.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -2,18 +2,11 @@ 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)))
    cat = ♯ getContents >>= (\cs → ♯ (putStr∞ cs))

    main : Prim.IO ⊤
    main = run cat
  3. puffnfresh created this gist Dec 7, 2016.
    19 changes: 19 additions & 0 deletions Main.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,19 @@
    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