我正在运行CoqIDE来阅读教科书系列“软件基础”,我目前正在阅读“逻辑基础”这一卷。我刚开始学习第二章(归纳),但当我尝试运行这行时 From LF Require Import Basics. 我得到一条错误语句 The file ...\LF\Basics.vo contains library Basics and not library LF.Basics 我尝试重命名该文件所在的目录,并重新编译缓冲区,但这些操作都没有帮助。我应该怎么做才能解决这个问题?
我很难理解如何在证明中使用我在Coq中定义的一些东西。Proof.induction n.simpl.
apply compress.现在,我明白了为什么我会出错,虽然从技术上来说,RepString n 0和s 0 (s 0 (s 0( ... s 0 E)))是一样的,但我根本找不到让coq知道的方法,我尝试了处理apply compress