@yosh as I understand it, it's a generalization of linearity with 0 uses meaning only available at compile time, 1 use meaning linearity and `w` (omega) being any number of uses (GC).

Idris2 is half theorem prover half programing languange so you can use Types as first level objects (e.g. similar to Zig, generic functions are just functions that return types). And you can also use most of the language at compile time.