В редакторе VSCode я ввёл такой код Lean4:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) :=
beginи получил "unknown identifier 'begin'". Если добавить end тремя строками ниже, появляется "invalid 'end', insufficient scopes". Что я сделал неправильно? Lean установлен некорректно?
In the VSCode editor, I entered this Lean4 code:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) :=
beginand got "unknown identifier 'begin'". Adding end three lines below gives "invalid 'end', insufficient scopes". What have I done wrong? Is my Lean installation incorrect?
Запись блоков begin/end относится к синтаксису lean 3. Для входа в режим тактик в Lean 4 используйте ключевое слово by, например:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := by sorryАналога end теперь нет, поскольку область определяется отступами, однако необязательный завершающий done выдаёт ошибку, если осталась незакрытая цель.
Даже при большом опыте с lean 3 я бы посоветовал просмотреть руководство (https://lean-lang.org/lean4/doc/) и/или Theorem Proving in Lean/Functional Programming in Lean (главы 4 и 5 руководства), учитывая значительные изменения и улучшения.
Ключевое слово end по-прежнему закрывает секции и пространства имён, чем и объясняется диагностика при использовании end здесь.
The begin/end block notation belongs to lean 3. To start tactic mode with Lean 4, use the keyword by, for example:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := by sorryThere is no corresponding end now because white space determines the scope, although an optional final done produces an error when a goal remains open.
Even with substantial lean 3 experience, I'd suggest looking through the manual (https://lean-lang.org/lean4/doc/) and/or Theorem Proving in Lean/Functional Programming in Lean (chapters 4 and 5 of the manual), given the considerable improvements and changes.
The end keyword still closes sections and namespaces, explaining the diagnostic you see when using end here.
Это означает, что Lean 4 установлен успешно, но его синтаксис не полностью совместим с Lean 3.
В дополнение к ответу hkr о by и необязательном done, тем, кто знаком с Lean 3, может пригодиться Lean 4 survival guide for Lean 3 users (https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users), где хорошо описаны основные различия.
It indicates a successful Lean 4 installation, whose syntax isn't entirely compatible with Lean 3.
Alongside hkr's answer about by and optional done, anyone who knows Lean 3 may find the Lean 4 survival guide for Lean 3 users (https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users) useful, as it provides a good account of the main differences.
Я новичок в функциональном программировании и пытаюсь создать функцию, которая принимает список значений (длина которого зара…
В последний раз я заглядывал в документацию JavaScript в 1996 году. Ищу учебный курс по “необходимому JavaScript и веб-концеп…
Многие примеры на go начинаются так : Мой GOPATH: Где хранятся main и модуль fmt?
