Tasiro

Idris allows very dependent types

2

This is essentially the same issue as in Agda (see https://github.com/agda/agda/issues/1556). *Very dependent types* allow an indexed type to use itself as an index. It can be quite useful, but...

Currently Lean code is folded like C code, where everything is folded until the next token with less indentation (usually the closing curly brace), including empty lines. That will fold...