mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 07:26:59 +03:00
4d0a065f86
To "interface/implementation". Old syntax is still valid but gives a deprecation warning. |
||
---|---|---|
.. | ||
corecords001.idr | ||
expected | ||
run |