小编use*_*753的帖子

有没有人有一小段代码来从 Coq 文件读取字符串(ynot库似乎这样做,但我无法弄明白)？

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" …