extracted/lists.mli

   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 all : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool
  30
  31 val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 val append : 'a1 List.list List.aop
  40
  41 val list : Monad.monadProps
  42
  43 val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
  44
  45 val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
  46
  47 val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
  48
  49 val ordered_insert :
  50   ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list
  51
  52 val insert_sort : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list
  53
  54 val range_strong_internal :
  55   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list
  56
  57 val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list
  58