idris-0.9.9.3: test/test031/test031.idr
module Main -- Test enabling the ErrorReflection extension %language ErrorReflection main : IO () main = return ()
module Main -- Test enabling the ErrorReflection extension %language ErrorReflection main : IO () main = return ()