Skip to content

Instantly share code, notes, and snippets.

@puffnfresh

puffnfresh/Main.agda

Created December 6, 2016 23:47
Show Gist options
  • Save puffnfresh/9563ff4d9657eedc0ffdc77faced679d to your computer and use it in GitHub Desktop.
Save puffnfresh/9563ff4d9657eedc0ffdc77faced679d to your computer and use it in GitHub Desktop.
Download ZIP
Non-terminating IO data type in Agda
Raw
Main.agda
module Main where
import IO.Primitive as Prim
open import Data.Unit
open import IO
open import Coinduction
nonTerminatingIO : IO ⊤
nonTerminatingIO = ♯ nonTerminatingIO >> ♯ return tt
main : Prim.IO ⊤
main = run nonTerminatingIO
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment