목록

Question

의 머리에 옵션 요소를 복용 내가 가진 유형

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. 

내 질문은 내가 전체 목록 l'에서 테스트하려는 때문에 테스트 if forallb (fun li => forallb (fun ci =>do_something ci d))ls)l' 내가 forallb (fun li =>...)을 추가 한 것입니다. 그러나 저는 인수 li을 전혀 사용하지 않았습니다.

편집 : 내 질문은 if forallb (fun li => forallb (fun ci => do_something ci d))ls)l'에 중점을 둡니다. 나는 l' 목록의 나머지 부분을 테스트하고 싶기 때문에 forallb (fun li =>을 추가했습니다. forallb (fun li이 없으면이 테스트 if (forallb (fun ci => do_something ci d))ls을 보관할 수 있지만 목록에서이 상태를 다시 테스트하는 방법을 모르겠습니다. l'.

Answer 1

컨텍스트가 일치하지 않습니다.

변수 난 : 목록 (리스트 L) : ...

가 난 목록

변수 LS가 있는지 확인합니다.

은 l이 유형이라고 가정합니다.

은 아마 당신은 의미 :

정의 L =리스트 (A * B를 * 옵션 C의 * 옵션 D).

변수 ls : = list (list l).

그러면 ls가 목록 목록 (3 차원 배열과 같은)의 목록이됩니다.

이제, l을 입력 할 do_something 것을 의미한다고 가정 -> D -> 부울

난 당신의 인수 LS에 입력 리터의 모든 요소와 유형 D의 모든 요소와 do_something 테스트하고 싶었 추측 테스트 (라고도 luck, yuck).

당신은해야

...

| 일부 D => 만약 forallb (재미 리튬 => forallb (재미있는 CI => do_something의 CI D)) 거짓 그 밖의 LS 다음 테스트 난 '. ..

그러나 솔직히 말해서, 귀하의 질문은 답변자가 추측하기에 충분합니다.