2

行列タイプはベクトルのリストです。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>
4

1 に答える 1

3

CoLoR ライブラリのことですよね?付随するRainbowライブラリをご覧になりましたか? XML プルーフ形式から Coq .v 仕様への変換はそこで行われ、ソースから簡単に理解できるはずです。

于 2013-06-17T03:25:46.553 に答える