Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
First reflected error in Idris
drc@drc:~/Documents/Code/Idris/error-reflection-test$ idris ErrorTest.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.10.1-git:5361547
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Type checking ./ErrorTest.idr
*ErrorTest> the Nat ""
ERROR HAPPENED!
*ErrorTest>
Bye bye
drc@drc:~/Documents/Code/Idris/error-reflection-test$ cat ErrorTest.idr
module ErrorTest
import Language.Reflection.Errors
%language ErrorReflection
total %error_handler
test : Err -> Maybe (List ErrorReportPart)
test a = Just [Message "ERROR HAPPENED!"]
total %error_handler
nothing : Err -> Maybe (List ErrorReportPart)
nothing a = Nothing
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.