ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-13 07:26:59 +03:00
Code Issues Projects Releases Wiki Activity
bde101fbd0
Idris-dev/test/syntax001
History
Edwin Brady 83f0af13fb Display expected type of RHS in error messages 
Also added %error_reverse annotations on IO so that IO related messages
are more readable. This improves the error in #2672.
2015-10-17 14:30:36 +01:00
..
expected Display expected type of RHS in error messages 2015-10-17 14:30:36 +01:00
run Replace absurd syntax rule FCs 2015-06-18 22:27:46 +02:00
Syntax.idr Better approximation of syntax rule errors 2015-06-18 22:52:26 +02:00
SyntaxOk.idr Better approximation of syntax rule errors 2015-06-18 22:52:26 +02:00
SyntaxTest.idr Replace absurd syntax rule FCs 2015-06-18 22:27:46 +02:00