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