source: driver/extracted/foldStuff.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 1.5 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Relations
12
13open Nat
14
15open Hints_declaration
16
17open Core_notation
18
19open Pts
20
21open Logic
22
23open Types
24
25open List
26
27open Util
28
29(** val foldl_strong_internal :
30    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
31    'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
32let rec foldl_strong_internal l h prefix suffix acc =
33  (match suffix with
34   | List.Nil ->
35     (fun _ -> Util.eq_rect_Type0_r prefix acc (List.append prefix List.Nil))
36   | List.Cons (hd, tl) ->
37     (fun _ ->
38       Logic.eq_coerc
39         (foldl_strong_internal l h
40           (List.append prefix (List.Cons (hd, List.Nil))) tl
41           (h prefix hd tl __ acc)))) __
42
43(** val foldl_strong :
44    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
45    'a2) -> 'a2 -> 'a2 **)
46let foldl_strong l h acc =
47  foldl_strong_internal l h List.Nil l acc
48
49(** val foldr_strong_internal :
50    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
51    'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
52let rec foldr_strong_internal l h prefix suffix acc =
53  (match suffix with
54   | List.Nil -> (fun _ -> acc)
55   | List.Cons (hd, tl) ->
56     (fun _ ->
57       h prefix hd tl __
58         (foldr_strong_internal l h
59           (List.append prefix (List.Cons (hd, List.Nil))) tl acc))) __
60
61(** val foldr_strong :
62    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
63    'a2) -> 'a2 -> 'a2 **)
64let foldr_strong l h acc =
65  foldr_strong_internal l h List.Nil l acc
66
Note: See TracBrowser for help on using the repository browser.