Idris 2 version 0.8.0 Released

[NewsBot]

A new Idris blog post/announcement has been posted!

A new version (0.8.0) of Idris 2 has been released. You can download the source (including generated Scheme and Racket files for bootstrapping) from the download page.

Highlights include:

• Autobind and Typebind modifier on operators allow the user to customise the syntax of operator to look more like a binder.
• Totality checking will now look under data constructors, so Just xs will be considered smaller than Just (x :: xs).
• Typst files can be compiled as Literate Idris.
• Constructors with certain tags (CONS, NIL, JUST, NOTHING) are replaced with _builtin.<TAG> (eg _builtin.CONS). This allows the identity optimisation to optimise conversions between list-shaped things.
• Refactored Uninhabited implementation for Data.List.Elem, Data.List1.Elem, Data.SnocList.Elem, and Data.Vect.Elem so it can be used for homogeneous (===) and heterogeneous (~=~) equality.
• The RefC backend compiler can emit precise reference counting instructions where a reference is dropped as soon as possible. This allows you to reuse unique variables and optimize memory consumption.
• Fix memory leaks of IORef in RefC backend. Now th...

Get the full details here: Idris 2 version 0.8.0 Released