s
Норм. Как вариант, можно ещё сделать многочлены с хвостом из нулей эквивалентными.
Size: a a a
2021 November 24
s
Можно доказывать алгоритмы без усечения и затем доказывать, что они инвариантны к усечению.
A
Что-то мне кажется теперь, что завтипострадания это не то, что нужно, когда есть Lean
s
В Lean тоже завтипы.
s
Просто ещё пара неконструктивных аксиом добавлена.
A
А, ок
Я с ним не знакомился, но видел примеры доказательств -- куда более читаемые
Я с ним не знакомился, но видел примеры доказательств -- куда более читаемые
s
Скажем так: коуравнители они by design немного боль. В любом формализме.
s
Это да, в лине есть тактики.
A
И кажется его как раз используют математики
A
В коке тоже ведь есть
A
Но там это больше напоминает какую-то нечитаемую формальную манипуляцию с целями
A
То есть без интерактивного прохода по доказательству ничего не понятно
s
Да, так. Доказательства на лине, кстати, можно писать столь же нечитаемым образом.
s
А можно взять show, have и фигурные скобки и сделать красиво.
s
А, ещё calc.
a
Бывает, что степень полинома неизвестна? Если известна, то ничего вручную усекать не должно быть нужно.
s
Ха, в лине всё намного проще сделано.
s
s
Просто функция с конечным носителем.
s