以選項元素列表

的頭我有型以選項元素列表

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'中再次測試此條件。

來源

2012-11-07 Quyen

什麼是定義中的'ls'？爲什麼內在的'forallb'？你的解釋很不明確，因爲你試圖達到的目標很不明確。 – Ptival

我編輯了我的問題。 – Quyen

您的上下文不一致。

變量L：...

使L是一個列表

可變LS：列表（表1）。

假設l是一種類型。

也許你的意思是：

定義L：=名單（A * B *選項C *選項d）。

變量ls：= list（list l）。

這使得ls成爲列表列表（如三維數組）。現在

，假設你的意思是do_something有L型 - > d - > BOOL

我想你想測試與L型的LS和的參數中的所有元素類型d的所有元素do_something測試（也叫l，yuck）。

你應該有

...

|一些d =>如果forallb（李樂趣=> forallb（CI樂趣=> do_something CI d））LS然後測試L」別的假。 ..

但坦率地說，你的問題留給回答者猜測！

來源

2012-11-08 13:52:56 Yves

以選項元素列表

回答

相關問題