[
Lets write some comments
Size: a a a
2021 May 31
KR
Как обычные функции, кмк. Хз в чём тут проблема.
[
Переслано от [BRM]White Rabbit
Кстати, я так и не выяснил, идрис оптимизирует числа пиано лишь для Nat или они научились редуцировать общий случай?
[
Переслано от Kir
Идрис - не знаю, в агде ты явно указываешь прагмой, какой из твоих типов будет оптимизированным Nat-ом
KR
Find usages, наверн, не работает
KR
@sand_witch пеано*
[
Ой, все
[
Буквоеды съели
p
Обычные функции обычно осмысленные. Вроде get_user который нужен в create_order который нужен в handle_request.
KR
Изи… просто коверкать имена - некрасиво.
[
У меня отвратительная память на имена
KR
Код-стайл и доки, никуда не деваются и с пруфами.
p
А зачем тебе не-Nat?
[
Я примерно месяц запоминал, как идрис пишется
[
Он жутко неэффективный. Во время дизайна норм, но рт предпочту без них
p
Идрис лишь проверка концепции. Не делай из него язык.
[
Ну, он декларируется как язык общего назначения
p
Декларация не означает правдивость. Это же маркетинг.
[
Т.е. мою киллер-либу, которая убьёт все другие языки, надо писать на хаскеле, а не на идрисе, так?