Я проходил курс по основам программного обеспечения и по какой-то причине мне НЕ удалось получить команду coqc для компиляции моих библиотек.
Я сделал:
coqc Maps.v
, но получил ошибку:
Ошибка: файл /Users/pinocchio/coq/software_foundations_vol1/Maps.vo содержит библиотекукарты, а не библиотека Карты
Я также пытался скомпилировать с помощью coqIDE, но получаю следующую ошибку:
Ошибка: Скомпилированная библиотека Maps (в файле / Users / pinocchio / coq/software_foundations_vol1/Maps.vo) делает противоречивые предположения относительно библиотеки Coq.Init.Notations
Любые идеи о том, что я могу сделать?