Coq正在使用类似于OCaml的模块系统。在OCaml中,我们可以应用像Module_A.Module_B.Func这样的函数,并使用Module_A.Module_B来查找到Func的路径。然而,我不能在Coq中做类似的事情。例如,如果我只运行Print Coq.Arith.Minus.minus_n_O.,Coq报告Coq.Arith.Minus.minus_n_O is not a defined object
我不太熟悉Coq中的模块,但它是在我最近提出的一个问题中提出的。我有下面的代码。Parameter n : nat.Coq在尝试运行n_plus_1时抱怨End ModuleInstance的定义。我不确定这是否是使用模块的正确方式,但我希望它只使用签名中的定义,这是一个不需要任何附加信息的完整定义</
从Coq中提取的Ocaml代码包括(在某些情况下)定义如下的类型__和函数__:let __ = let rec f _ = Obj.repr f in Obj.reprf
文档说,在过去,这种类型被定义为unit (因此__可以被视为()),但是存在(很少)将__类型的值应用于__类型的值的情况。__使用了OCaml中未记录的Obj模块函数,但似乎定义的<