source: driver/extracted/lists.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: 2.3 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29(** val all : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
30let rec all p = function
31| List.Nil -> Bool.True
32| List.Cons (h, t) -> Bool.andb (p h) (all p t)
33
34(** val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
35let rec map_All f l =
36  (match l with
37   | List.Nil -> (fun _ -> List.Nil)
38   | List.Cons (hd, tl) -> (fun _ -> List.Cons ((f hd __), (map_All f tl))))
39    __
40
41open Setoids
42
43open Monad
44
45open Option
46
47(** val append : 'a1 List.list List.aop **)
48let append =
49  List.append
50
51(** val list : Monad.monadProps **)
52let list =
53  Monad.makeMonadProps (fun _ x -> List.Cons (x, List.Nil)) (fun _ _ l f ->
54    List.foldr (fun x -> List.append (f x)) List.Nil l)
55
56(** val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
57let rec count f = function
58| List.Nil -> Nat.O
59| List.Cons (x, l') ->
60  Nat.plus
61    (match f x with
62     | Bool.True -> Nat.S Nat.O
63     | Bool.False -> Nat.O) (count f l')
64
65(** val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
66let position_of_safe test l =
67  Option.opt_safe (List.position_of test l)
68
69(** val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
70let index_of test l =
71  position_of_safe test l
72
73(** val ordered_insert :
74    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list **)
75let rec ordered_insert lt a = function
76| List.Nil -> List.Cons (a, List.Nil)
77| List.Cons (h, t) ->
78  (match lt a h with
79   | Bool.True -> List.Cons (a, (List.Cons (h, t)))
80   | Bool.False -> List.Cons (h, (ordered_insert lt a t)))
81
82(** val insert_sort :
83    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
84let rec insert_sort lt = function
85| List.Nil -> List.Nil
86| List.Cons (h, t) -> ordered_insert lt h (insert_sort lt t)
87
88(** val range_strong_internal :
89    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list **)
90let rec range_strong_internal index how_many end0 =
91  (match how_many with
92   | Nat.O -> (fun _ -> List.Nil)
93   | Nat.S k ->
94     (fun _ -> List.Cons (index,
95       (range_strong_internal (Nat.S index) k end0)))) __
96
97(** val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list **)
98let range_strong end0 =
99  range_strong_internal Nat.O end0 end0
100
Note: See TracBrowser for help on using the repository browser.