4 ms·
They mean dependent types, in the Idris sense. Basically, types (not just instances of types i.e. the entire collection `int` rather than 5) are first-class cit
by AkshatM 5y ago
They mean dependent types, in the Idris sense. Basically, types (not just instances of types i.e. the entire collection `int` rather than 5) are first-class citizens that can be passed to functions. It enables proof checking as well as so-called "type-driven development".