AN
Но это не интересно нужно where b : Lt<a>, а не просто константы
Size: a a a
2021 May 29
gо
А какая разница?
gо
Будет, типа, Refined(int, Lt(a)), где a — уникальный тип
AN
может и нет разницы. я так чисто по приколу сказал. Для пользователя есть разница.
ΑZ
Нет
ΑZ
Констэкспр например рантайм не требует
gо
Он и не самостоятельный
p
Как привязать Lt к операции < ?
ΑZ
Пруфы и типы это синонимы
ΑZ
Ну так можно только подмножество сделать
gо
А это мы и обсуждали
AN
ну для констант это допустим само проверяется. Иначе два пруфа требуешь
AN
Но мне кажется нету смысла это хардкодить таким образом, потому что можно на какой то более базовой аксиоматике построить доказательство что операция ">" транзитивна. Потому что иначе как то много хардкодить надо. Допустим что делать чтобы доказать что a < b, c < d => a + c < b + d?
ΑZ
прост есть уже идрис
ΑZ
там все продумано и кмк все разумно
AN
но нет плейграунда ) зато у LiquidHaskell есть. М -маркетинг.
H
надо сделать плейграунд для metalang99
p
а еще стандарт и утвердить в ISO
