X
когда у тебя контекста хватает
Size: a a a
2021 December 01
X
тогда работает
X
лично тебе
X
а у него контекста существенно меньше
X
и способности к восстановлению значения неизвестного слова тоже
a
Я уже жаловался на это :-(
ГG
Ну, это типикал случай
V🇺
2021 December 02
X
ну что ж, рекурсивные доказательства в F* ещё очень даже ничего так)
X
сижу ковыряюсь с полиномами, потихоньку картинка складывается
s
Рекурсивное доказательство может быть даже удобнее, чем соответствующая тактика.
X
я опасался, что ему надо будет слишком разжёвывать
X
а оказалось что он прекрасно врубается
X
если дальше так пойдёт, то базовые вещи про многочлены я быстро докажу и кольца построю
s
Бета-редукция это одна из мощнейших автоматизаций, да.
s
При всей своей простоте.
s
Собственно тройка вычисление — simp — auto решает большинство проблем.
s
auto, правда, далеко не везде есть.ДГ
Что-то я совсем запутался
Можете объяснить, пожалуйста
Можете объяснить, пожалуйста
i
Вы что говорите