Тем более

Вот бы мне к F* привыкнуть

Сложна?

КМК, про индуктивное доказательство они явно чересчур сложно рассказали

Даже с тем фактом, что сам принцип я знаю и доказывал не раз

Ты конечно права, но есть неотъемлемый объём работы, который ты должна будешь делать в ATS, и который не нужно делать скажем в Хаскеле - я о доказательствах. Написание доказательств мне напоминает написание программ на динамическом языке с причудливым синтаксисом и без возможности отладки. То есть некий текст, который надо написать правильно для сигнатуры каждой функции, причём вход не всегда понятен, а выходом является сообщение об ошибке.

https://www.fstar-lang.org/tutorial/

Секция 3.3.3. A simple lemma proved by induction, in detail

Тоже верно, зато дебажить не надо!)

Я дополнил сообщение.

В общем, как-то непонятно и непоследовательно

Ну для меня тоже сложно, но я пока не в особо в теме)

Наверное если бы я работал на хаскеле, то интересовался бы и фистаром и АТС. А так, надо вникать в оторванную от практики область😊

От моей практики то есть

Торт ты шаришь за фистар?

Если кто-то в чате шарит за F* (думаю, кто в общем про ФП шарит, тот разберётся), буду благодарен, если объясните _пошагово_ как мы это свойство доказали для факториала и что должны делать мы, а что Z3

"непонятно и не симметрично"

А что несимметрично?

Я вообще не вижу связи между ответом к задаче и выкладками

И я