Устранение ошибки «Неправильное начало версии c» в CoqIDE 8.11 с функциональной схемой - PullRequest
Новая
       59

Устранение ошибки «Неправильное начало версии c» в CoqIDE 8.11 с функциональной схемой

0 голосов
/ 14 марта 2020

Я как-то новичок в Coq, использую CoqIDE 8.11, и не вижу, что я здесь сделал неправильно. Я проверил документацию , но не смог найти решение моей проблемы.

С 

Functional Scheme insert_ind := Induction for insert Sort Prop.
Check insert_ind.

Я получил сообщение Syntax error: illegal begin of vernac.. Знание, что вставка ранее была определена следующим образом: 

Fixpoint insert l a :=
match l with
| nil => (a::nil)
| (b::l) =>
  match preOrdreImplem a b with
  | true => a::b::l
  | false => b:: (insert l a)
  end
end.

И что я использовал ее в части леммы и не столкнулся с проблемой. Любая помощь или подсказка высоко ценится.

...