mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-18 18:31:43 +03:00
728ef085a5
For the types of local names, don't write out the environment - it's going to be repeated for every name, mostly it's unhelpful, and if you want to see the types of other names you can ask directly. This can save a huge amount of time when environments are slightly complicated. |
||
---|---|---|
.. | ||
expected | ||
input | ||
LocType.idr | ||
run |