Как решить очень простую синтаксическую ошибку: «конец» ожидается после [веток] (в [term_match]). в Коке? (в Галлине, а не в лтаке)
Я пытался написать очень простую программу для суммирования nats в списке (копипаст отсюда):
Fixpoint sum (l : list nat) : nat :=
match l with
| [] => 0
| x :: xs => x + sum xs
end.
но мои локальные Coq и jsCoq жалуются:
Syntax error: 'end' expected after [branches] (in [term_match]).
Почему это? (обратите внимание, я даже не реализовал это, но моя реализация выглядит почти так же)
Я реализовал рекурсивные функции раньше:
Inductive my_nat : Type :=
| O : my_nat
| S : my_nat -> my_nat.
Fixpoint add_left (n m : my_nat) : my_nat :=
match n with
| O => m
| S n' => S (add_left n' m)
end.
который не жалуется...
Я видел этот вопрос Как сопоставить выражение "match"?, но, похоже, он касается какой-то особой проблемы в ltac, а я не использую ltac.
Ответы 2
Расположение ошибки находится на [], что говорит о том, что Coq не понимает эту запись. Обнаружив неопределенную нотацию, синтаксический анализатор понятия не имеет, что делать, и выдает по существу бессмысленное сообщение об ошибке.
Чтобы определить стандартную нотацию списка, вам необходимо импортировать ее из стандартной библиотеки через:
Require Import List.
Import ListNotations.
Модуль stdlib List содержит модуль ListNotations, который определяет [] (и, в более общем смысле, [ x ; y ; .. ; z ]). List также определяет обозначение x :: xs.
@Yves Хорошо, надеюсь, теперь это будет менее сложно, поскольку они могут найти ошибку в Google (когда произошла моя ошибка, в Google ничего не было полезно). Но этот вопрос и ответ, надеюсь, изменят это :)
Я только что добавил свой собственный ответ, но я думаю, что было бы лучше, если бы что-то подобное было включено в ответ @mudri.
при подборе выдержек из разработки вам также необходимо выяснить, какие команды изменения синтаксиса влияют на эти выдержки: импорт модулей, открытие области видимости, объявления аргументов (для имплицитных), нотации и приведения ». В данном случае , файл фактически предоставлен автором упражнений через этот указатель.
Тот факт, что синтаксис на самом деле зависит от того, какие модули вы загрузили, вызывает сожаление. Раньше мне и в голову не приходило, что это может так расстраивать людей, желающих выучить язык.