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