Здравствуйте, varenikAA, Вы писали:

AA>Тут сказано используйте схему для сборки идрис2 или можете пойти жестким путем через бутстрапиннг.
AA>по умолчанию правда не ракет, а чес-схем.

Там забавные вещи пишут:

> This includes Scheme source as generated by Idris

Получается, что не Racket (который позиционируют как "Language-Oriented Programming Language") используется для генерации кода, а наоборот: идрисом генерят код на схеме?..