mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-18 18:31:43 +03:00
751fd1f36a
If unelaborating a term that's just a hole, show the scope it was created in too, to help with error messages |
||
---|---|---|
.. | ||
Dots1.idr | ||
Dots2.idr | ||
Dots3.idr | ||
expected | ||
run |