NobbZ/main.idr

Last active August 29, 2015 14:02

Star (0) You must be signed in to star a gist
Fork (0) You must be signed in to fork a gist

Select an option

Learn more about clone URLs
Clone this repository at <script src="https://gist.github.com/NobbZ/68ea30b8e323ceafd212.js"></script>
Save NobbZ/68ea30b8e323ceafd212 to your computer and use it in GitHub Desktop.

Download ZIP

Does not compile because `main` does not see `y`

Raw

	module Main

	main : IO ()
	main = putStrLn (show y)

	y : Int
	y = 1

NobbZ commented Jun 12, 2014

Author

Trying to compile the above yields following message:

$ idris main.idr -o test
main.idr:4:23:When elaborating right hand side of main:
When elaborating an application of function Prelude.show:
        No such variable y

$ idris --version
0.9.13.1

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment