Yes! - Idris' `String` type is not just a list of characters, here [1] you can see some relevant functions, I'm still trying to find the definition of `String`

Yes! - Idris' `String` type is not just a list of characters, here [1] you can see some relevant functions, I'm still trying to find the definition of `String` though. - Functions can be overloaded in Idris, which enables declaring a field with the same name on different records. I'm not sure what you mean with modules and namespacing though [1] https://www.idris-lang.org/docs/current/prelude_doc/docs/Prelude.Strings.html https://www.idris-lang.org/docs/current/prelude_doc/docs/Pre...