AG
обычно стягивают не все конструкторы, а какие то полезные их комбинации
Size: a a a
2020 December 04
AG
как вон в OddList из второй ссылки
к
или как -0 = +0 в моем не самом удобном для работы int
к
это как бы склеит два множества интов в одной из точек
к
как например склеиваются 1/2 и 4/8
к
это тоже разные термы
AG
точнее склеит два множества натов в инты
к
но аксиоматически они равны
ХГ
на самом деле достаточно тупой сюжет у Хранителей, для меня они вытягивают только на Роршахе и художественном стиле
Имел в виду Толки(е)на. А про Роршаха Рондарев недавно задвигал...
DB
ща пажадите, я отвклёкся...
AC
Имел в виду Толки(е)на. А про Роршаха Рондарев недавно задвигал...
а, Хранители Кольца
к
data Rational where
rat : Int -> Nat -> Rational
reduce : forall n m c, rat (c * n) (c * m) = rat n m
rat : Int -> Nat -> Rational
reduce : forall n m c, rat (c * n) (c * m) = rat n m
DB
вообще говоря вот эти аксиомы понял, но точки пока всё равно не понял)
DB
надо про точки почтитать что ле
к
точки это просто значения от 0 до 1 в R например
к
в кубиках там не так
DB
а как
к
там свободная деморгана алгебра, а в arend просто юнит, где две точки, которые равны друг другу
AG
не, вообще интервалы как раз в кубах появляются
AG
просто они там по разному устроены в разных диалектах