r
Или не то. Всё-таки иногда
assert_eq!(f(4), 100500) полезенassert_eq!(f(4), 100500) полезенSize: a a a
2020 August 24
ΑZ
red75prime
Или не то. Всё-таки иногда
ну так ты можешь написать
typelevelAssert : f 4 -> 100500r
Доказать type-level assert
ΑZ
red75prime
Доказать type-level assert
typelevelAssert : (x : f 4) -> x = 100500
typelevelAssert 100500 = Refl
Что-то в таком духеr
Плюс доказательство тотальности
CD
если юзать их неправильно то они не всел овить будут, очевидно
ну давай я тебе объясню про кэши, а ты мне объяснишь, как правильно юзать
CD
есть уровень Data и три уровня кэша - Addressable, PreRenderer и Renderer
последние два нас сейчас не интересуют
на уровне Addressable построены индексы для поиска, как можно догадаться из названия, адресов
Addressable - естественная граница иммутабельности для того же абзаца
последние два нас сейчас не интересуют
на уровне Addressable построены индексы для поиска, как можно догадаться из названия, адресов
Addressable - естественная граница иммутабельности для того же абзаца
CD
содержимое редактора это гетерогенное дерево, интерпретация узлов контекстно-зависимая (как минимум от предков), поэтому selection определён чтобы сохраняться для контекстно-независимого элемента
CD
это условно путь в дереве + хвост, состоящий из пары локальных точек + вектора точек расширения, который нас не интересует
CD
точка это пара чисел, причём второе не участвует в сравнении (оно нужно только для позиционирования каретки)
ΑZ
red75prime
Плюс доказательство тотальности
ну это не так сложно
ΑZ
в крайнем случае можно читерить с Fuel
ΑZ
ну давай я тебе объясню про кэши, а ты мне объяснишь, как правильно юзать
сори, нет
ΑZ
мне работать тоже надо
ΑZ
хочешь оставайся при своем
CD
сори, нет
ну до этого момента утверждение "тут всё можно разрулить" оно очень голословное
CD
потому что ты споришь с примером, который у меня перед глазами
CD
и утверждаешь, что он не существует
ΑZ
ну до этого момента утверждение "тут всё можно разрулить" оно очень голословное
нет, просто некоторые вещи в типах делать дорого
ΑZ
и часто людей не интересует что система не работает совсем правилньно во всех случаях