One of the best features of Idris 2 has nothing to do with its dependent types or quantities or proof search: it's the standard library which is very much like a cleaned-up Haskell standard library, with proper overloading to avoid naming conflicts, and even the ability to select among multiple interface implementations for the same type.
For some simple examples see https://github.com/stefan-hoeck/idris2-tutorial