G
А, это что ли кайнд типа данных
Size: a a a
2020 March 15
G
Круто
p
Т-34 85
норм??? это 7 win xp запущенных
Мне норм
AZ
@Psilon
https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Functor.idr#L10
Почему
https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Functor.idr#L10
Почему
(f: Type -> Type), а не просто f?
в хаскелле ты так же можешь написать по идее
G
в хаскелле ты так же можешь написать по идее
Не знал
G
Но мне нравится, что Idris заставляет прописывать типы
В
Но мне нравится, что Idris заставляет прописывать типы
Только это же не тип
G
В объявлениях функций он заставляет это делать
G
А в объявлениях интерфейсов заставляет кайнды прописывать
В
Ясно
G
Потом можно просто нажать Ctrl+A и он сгенерирует определение
В
xd
G
Потом Ctrl+C и сгенерирует сопоставление по образу
G
Ты просто заделываешь так называемые unimplemented!() и код готов
G
Вот бы в Rust такую штуку
В
Ну идея умеет все варианты енама в матч подставлять
G
Не знал
G
Получается генерация определения и так есть (нам его в Rust не нужно генерировать), генерация
match есть, doc естьВ
Получается генерация определения и так есть (нам его в Rust не нужно генерировать), генерация
match есть, doc естьА в идрис зачем определение нужно генерить?