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

Question

我有一个矩阵类型是一个向量列表。 vector 是一个整数列表。它位于 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 规范的转换发生在那里，您应该能够轻松地从源代码中找出它。