xsd - 将 XSD 中的列表读取到 OCaml 和 Coq 中的列表

Question

我有一个矩阵类型是向量列表。向量是一个整数列表。它在 XSD 数据结构中。我想知道数据结构是如何读取这个构造函数的，是从上到下还是从下到上读取？更具体我想知道这个列表在 Coq 和 OCaml 中的样子。据我了解：

我将有一个列表列表：matrix = [[1 :: 0 :: nil] :: [0 :: 0 :: nil] :: nil]

我只是想确保我的理解。你能向我澄清一下吗？非常感谢。

 <matrix>
    <vector>
     <coefficient>
        <integer>1</integer>
      </coefficient>
      <coefficient>
        <integer>0</integer>
      </coefficient>
   <vector>
      <coefficient>
        <integer>0</integer>
      </coefficient>
      <coefficient>
        <integer>0</integer>
      </coefficient>
    </vector>
 </matrix>

Answer 1

你说的是 CoLoR 库，对吧？你看过它附带的Rainbow库吗？从 XML 证明格式到 Coq .v 规范的转换发生在那里，您应该能够轻松地从源代码中找出它。