CD
таблица выполняла ту же операцию, только после этого выполняла еще преобразование LocalSelection -> LocalTableSelection
Size: a a a
2020 August 24
ΑZ
короче, любую ошибку в рантайме можно записать в типы
ΑZ
не всегда это целесообразно
ΑZ
но возможно всегда
CD
короче, любую ошибку в рантайме можно записать в типы
так нет ошибки в рантайме
CD
нарушено примерно следующее утверждение
CD
для любого возможного LocationChild элемента Child, который лежит внутри таблицы Location, и любого GlobalSelection, верна импликация (GlobalSelection.Here(LocationChild) != None) -> (LocalTableSelection(GlobalSelection.Here(Location)).Contains(Child))
DF
Ну так зависимые типы равномощны логике
CD
я тут еще сомневаюсь, как это вообще формулировать, потому что LocalTableSelection может проверять локальную координату, которую надо получить операцией из Location и LocationChild, которая никогда не используется
CD
вопрос в том
CD
для любого возможного LocationChild элемента Child, который лежит внутри таблицы Location, и любого GlobalSelection, верна импликация (GlobalSelection.Here(LocationChild) != None) -> (LocalTableSelection(GlobalSelection.Here(Location)).Contains(Child))
как только такое утверждение записано, одного взгляда достаточно, чтобы понять, что оно сломается
CD
написать это утверждение равносильно не сделать ошибку в спеке
ΑZ
давай начнем с простого
ΑZ
ошибку в спеке детектировать невозможно
ΑZ
это информация внешняя для системы
ΑZ
и одно и то же поведение с точки зрения одного аналитика будет правильно, а другого - ошибочное
CD
ошибку в спеке детектировать невозможно
Конечно, возможно, я сделал это одним взглядом на (не)работающую систему
ΑZ
Конечно, возможно, я сделал это одним взглядом на (не)работающую систему
как ты определил что она не работает?
CD
как ты определил что она не работает?
ну я увидел, что внутри ячейки (1,3) нарисован выделенный символ конца параграфа и очень сильно зачесал репу
ΑZ
ну я увидел, что внутри ячейки (1,3) нарисован выделенный символ конца параграфа и очень сильно зачесал репу
так может так и надо?