mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 10:18:23 +03:00
ebc413ede5
It's worth delaying in case doing some more work (and some more interface resolution) can make the type more concrete. This makes test linear011 work more smoothly, and will help with this sort of program in general. A better way, later, would be to try elaborating and delay only if the type is not yet known. We have the facilities, but it's too fiddly for me to want to implement it right now... |
||
|---|---|---|
| .. | ||
| base | ||
| contrib | ||
| network | ||
| prelude | ||