https://github.com/idris-lang/Idris2/issues/725
Imagine advertising complete type safety, dependent types and complete typechecking and ending up with this.
This would never happen in Anaconda Scheme.
>>2
Idris2 is bootstrapped in Scheme:
https://raw.githubusercontent.com/idris-lang/Idris2/master/bootstrap/idris2_app/idris2.ss <-- entire Idris program