1

Coqがこれを受け入れないのはなぜですか？

Notation "[ d1 , .. , d2 ]" := (addition (multiply ( .. d1 .. ) ten) d2).
4

1 に答える 1

2

再帰表記は、かなり厳格な規則に従う必要があります。繰り返すパターンは2回表示する必要があります（これにより、Coqは何を繰り返すかを認識します）。1回d2は穴の周りを使用し、もう1回は終了式d1の周りを使用します。穴の周りを使用して、パターンを1回だけ使用しました。（リストの表記法のように）いくつかの周りに別の反復が必要です。d2zeronil

Notation "[ d1 , .. , d2 ]" :=
  (addition (multiply .. (addition (multiply zero ten) d1) .. ten) d2).

ゼロを導入したくない場合は、角かっこ内に少なくとも2桁（上記の1桁ではなく）を必要とし、それを終了式として使用できます。これは、ペアの表記法に似ています（でInit/Notations.v、マニュアルにも記載されています）。[d0]これを優先度の低い表記で補完することもできますが、これはd0あまり意味がありません。

Notation "[ d0 , d1 , .. , d2 ]" :=
  (addition (multiply .. (addition (multiply d0 ten) d1) .. ten) d2).
于 2012-08-31T15:18:19.267 に答える