0

私はタイプを持っています

Variable l: list (a * b * option c * option d).
Variable ls : list (list l).

リストの先頭からタイプを取得し、option dその後リスト全体を確認したいと思います。私のコードは次のようになります。

Definition test (l: list (a * b * option c * option d)):=
match l with
| nil => ... (* not important *)
| (_,_,_,od) :: l' => 
  match od with
  | None => ... (* not important *)
  | Some d => if forallb (fun li => forallb (fun ci => do_something ci d)) ls) l'
  end
end.

私の質問は、リスト全体でテストしたいので、if forallb (fun li => forallb (fun ci =>do_something ci d))ls)l'追加したテストです。しかし、私はその議論をまったく使用しませんでした。forallb (fun li =>...)l'li

編集：私の質問はに焦点を当てていif forallb (fun li => forallb (fun ci => do_something ci d))ls)l'ます。forallb (fun li =>リストの残りの部分でテストしたいので、追加しましたl'。このテストforallb (fun liをアーカイブすることはできif (forallb (fun ci => do_something ci d))lsませんが、リストでこの状態を再度テストする方法がわかりませんl'。

4

1 に答える 1

0

あなたの文脈は矛盾しています。

変数 l : ...

l をリストにする

変数 ls : リスト (リスト l)。

l が型であるとします。

多分あなたは意味した：

定義 l := リスト (a * b * オプション c * オプション d)。

変数 ls := リスト (リスト l)。

これにより、ls がリストのリストのリストになります (3 次元配列のように)。

ここで、do_something の型が l -> d -> bool であると仮定したとします。

ls の型 l のすべての要素と test の引数の型 d のすべての要素 (l、yuck とも呼ばれます) で do_something をテストしたかったと思います。

あなたが持っている必要があります

...

|Some d => if forallb (fun li => forallb (fun ci => do_something ci d)) ls then test l' else false ...

しかし、率直に言って、あなたの質問は回答者が推測する余地がたくさんあります!

于 2012-11-08T13:52:56.083 に答える