шаблон согласования списка список

Question

У меня есть list list nat Я хочу, чтобы написать функцию, чтобы разобрать в этом списке, например:

Definition my_function (l : list list nat) := 
let fix aux acc l := 
    match l with 
    | nil => acc 
    | c :: l' => match c with 
       | nil => acc 
       | d :: l'' => aux d l' 
       end 
    end in aux 0 l. 

Здесь я не знаю, как я могу использовать l''. Есть ли лучший способ написать эту функцию? Большое спасибо.

EDIT: Я хочу знать об алгоритме, который я могу проверить весь список l.

Answer 1

Я не понимаю, что ваша функция должна выполнить, но он должен иметь такую ​​форму:

Axioms (s1 s2 s3 : Set) (f3 : s3) (f4 : s1 -> s3 -> s3) (f1 : s2) 
    (f2 : s3 -> s2 -> s2). 

Fixpoint my_funct_aux (l1 : list s1) : s3 := 
    match l1 with 
    | nil  => f3 
    | cons e1 l2 => f4 e1 (my_funct_aux l2) 
    end. 

Fixpoint my_funct (l1 : list (list s1)) : s2 := 
    match l1 with 
    | nil  => f1 
    | cons l2 l3 => f2 (my_funct_aux l2) (my_funct l3) 
    end. 

Или, если вы не возражаете terseness:

Axioms (s1 s2 s3 : Set) (f3 : s3) (f4 : s1 -> s3 -> s3) (f1 : s2) 
    (f2 : s3 -> s2 -> s2). 

Fixpoint fold {s1 s2 : Set} 
    (f1 : s2) (f2 : s1 -> s2 -> s2) (l1 : list s1) : s2 := 
    match l1 with 
    | nil  => f1 
    | cons e1 l2 => f2 e1 (fold f1 f2 l2) 
    end. 

Definition my_funct : list (list s1) -> s2 := 
    fold f1 (fun l1 l2 => f2 (fold f3 f4 l1) l2).