Thoughts
Idris attempts to solve the same problem as [Thu](https://ourjseditor.com/program/S5ShEy). They're just doing it very differently.
Idris pulls types into the main scope, which is something that I avoided with Thu. But I still treat Types very dynamically in Thu, kind of adding dynamic operators to the type scope.