1

WITH構成は、最大 8 つの変数に対してのみ定義されます。どうすれば 8 個以上を使用できますか? 例：

Definition find_key_spec :=
  DECLARE _find_key
    WITH sh : share, m : ArrMapZ, start : Z, key : Z, i : nat,
         vbb : val, vkeys : val, vstart : val, vkey : val, vi : val
    PRE ...

=>

Toplevel input, characters 176-177:
Syntax error: 'PRE' '[' expected after [constr:operconstr level 200]
(in [constr:binder_constr]).

私が使用するもの: VST 1.5 (2014-10-02 で 6834P)、CompCert 2.4、Coq 8.4pl3(Jan'14) with OCaml 4.01.0。

4

2 に答える 2

1

別の方法として、WITH 句にタプルを導入し (例: WITH x12: (t1 * t2)%type)、射影によって PRE および POST のコンポーネントを参照します (例: PRE の x1 の代わりに fst x12 を使用します)。

于 2015-01-26T19:18:37.563 に答える