mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-29 07:44:45 +03:00
e1c6926da6
They're global, and so we don't reset per file, so we might get duplicates, so it's much quicker to store as a map even though we'd expect few of them overall. |
||
---|---|---|
.. | ||
base | ||
contrib | ||
network | ||
prelude |