ΑZ
с чего ты взял?
Size: a a a
2020 August 24
CD
с чего ты взял?
с того, что нет противоречия
CD
корректная программа может так себя вести
ΑZ
как ты определил что не может?
CD
как ты определил что не может?
система типов запрещает мне писать логически непротиворечивые программы?
ΑZ
что мешает в типах определить:
foo : (sel : Selection (a, b) (c, d))
-> (points : List Points ** All Points (\p -> contains sel p)
?CD
что мешает в типах определить:
foo : (sel : Selection (a, b) (c, d))
-> (points : List Points ** All Points (\p -> contains sel p)
?есть два определения "выделено", одно пойдёт ли туда сообщение to selected (для себя), второе считает ли потомок себя выделенным (для потомка), они не связаны
ΑZ
Определи два типа Selection для каждого вида "Выделено"
CD
Определи два типа Selection для каждого вида "Выделено"
так все, потомок считает, что выделен в положении (1, 3)
CD
таблица так не считает
CD
мы видим чудесный баг на выходной сцене
B
нет, просто я не вижу смысла запускать кривую нерабочую программу
Ну виндой люди пользуются, хотя там багов хватает)
B
Ну в линухе тоже
(На десктопах)
(На десктопах)
ΑZ
мы видим чудесный баг на выходной сцене
ну ты использвал тип SelectionPosition вместо SelectionInheritance
ΑZ
получил бы ошибку компиляции
CD
получил бы ошибку компиляции
где
CD
они и так разные
CD
потомок выполнил операцию GlobalSelection.Here(Location)
CD
получил LocalSelection, полностью его покрывающий