mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-18 02:11:32 +03:00
471a47255f
Data types with one constructor, that has one unerased argument, are translated to that argument for runtime. This doesn't have a huge effect on its own, but doing this will expose other optimisations later (e.g. increasing effect of inlining).
15 lines
407 B
Markdown
15 lines
407 B
Markdown
Changes since Idris 2 v0.1.0
|
|
----------------------------
|
|
|
|
Compiler updates:
|
|
|
|
* Data types with a single constructor, with a single unerased arguments,
|
|
are translated to just that argument, to save repeated packing and unpacking.
|
|
(c.f. `newtype` in Haskell)
|
|
|
|
Changes since Idris 1
|
|
---------------------
|
|
|
|
Everything :). For full details, see:
|
|
https://idris2.readthedocs.io/en/latest/updates/updates.html
|