Idris2-boot/tests/idris2/interface003
Edwin Brady 14e9872f07 Don't show MN names in hole contexts
This prevents display of shadowed names from case blocks/where clauses
that are now unusable. It does mean that constraint arguments aren't
displayed, unless given an explicit name - this may not be good, since
we might want to know which constraints are in scope, so it may yet need
a little tweaking.
2020-02-15 22:33:13 +00:00
..
Do.idr More interface tests 2019-06-24 18:04:43 +01:00
expected Don't show MN names in hole contexts 2020-02-15 22:33:13 +00:00
input More interface tests 2019-06-24 18:04:43 +01:00
run Add '--no-banner' option 2019-09-24 20:26:25 +06:00