有没有人能用一小段代码从Coq中的文件中读取字符串（ynot库似乎可以做到这一点，但我不知道）？
可以在这里找到：http://ynot.cs.harvard.edu/
该发行版在示例中包含一个IO目录，其中包括FS.v，它定义了以下内容：
Fixpoint ReadFile (fm : fd_model) (ms : list mode) (fd : File fm ms) (str : string) {struct str} : Trace :=
match str with
| EmptyString => Read fd None :: nil
| String a b => (ReadFile fd b) ++ (Read fd (Some a) :: nil)
end.
但是我不知道如何调用它。
我已经尝试过类似的事情：
Eval compute in ReadFile (File (FileModel "demo.txt") [R]).
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The term "File (FileModel "demo.txt") [R]" has type "Set" while it is expected to have type "File ?16 ?17".
类似地，Quark项目（http://goto.ucsd.edu/quark/）用替代机制定义了
VCRIO.v。任何帮助将非常感激！
最佳答案
通常，由于基本语言Gallina是纯净的和完全的，您将无法直接在Coq内部执行文件I / O。
特别是，您正在查看的函数ReadFile不是读取文件的函数，而是计算由读取文件的操作生成的跟踪的函数。
我们在Quark（及其后续项目Reflex http://goto.ucsd.edu/reflex）中解决此问题的方法是，对这些有效动作进行公理化，例如，请参见第323行的https://github.com/UCSD-PL/kraken/blob/master/reflex/coq/ReflexIO.v了解我们的原语的公理化类型。
因此，在Coq方面，我们推理使用此一元有效类型，然后在提取代码后，使用适当类型的OCaml函数实现这些公理，请参见此处
https://github.com/UCSD-PL/kraken/blob/master/reflex/ml/primitives/ReflexImpl.ml第111行。
显然，这增加了您值得信赖的计算基础，因为您需要确保原语完全符合公理化的要求，而不再需要其他任何工作。
回顾一下，我们无法在Gallina本身中执行有效的操作，因此我们将这些操作公之于众，并且只能使用提取的OCaml代码真正执行它们。
我不知道有什么技术可以让您在Gallina内部使用丰富的类型来完成这些工作。
关于io - 通过ynot在Coq中进行文件I/O，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/25022919/