mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 07:26:59 +03:00
e90316a5e1
Now, code blocks that are declared to be Idris code (with the Markdown language specifier) are type checked, and any type checker or parser errors that occur are retained and displayed to IDEs. |
||
---|---|---|
.. | ||
expected | ||
input | ||
interactive005.idr | ||
run |