extracted/list.mli

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Bool
  14
  15 open Relations
  16
  17 open Nat
  18
  19 type 'a list =
  20 | Nil
  21 | Cons of 'a * 'a list
  22
  23 val list_rect_Type4 :
  24   'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
  25
  26 val list_rect_Type3 :
  27   'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
  28
  29 val list_rect_Type2 :
  30   'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
  31
  32 val list_rect_Type1 :
  33   'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
  34
  35 val list_rect_Type0 :
  36   'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
  37
  38 val list_inv_rect_Type4 :
  39   'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  40   'a2
  41
  42 val list_inv_rect_Type3 :
  43   'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  44   'a2
  45
  46 val list_inv_rect_Type2 :
  47   'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  48   'a2
  49
  50 val list_inv_rect_Type1 :
  51   'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  52   'a2
  53
  54 val list_inv_rect_Type0 :
  55   'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  56   'a2
  57
  58 val list_discr : 'a1 list -> 'a1 list -> __
  59
  60 val append : 'a1 list -> 'a1 list -> 'a1 list
  61
  62 val hd : 'a1 list -> 'a1 -> 'a1
  63
  64 val tail : 'a1 list -> 'a1 list
  65
  66 val option_hd : 'a1 list -> 'a1 Types.option
  67
  68 val option_cons : 'a1 Types.option -> 'a1 list -> 'a1 list
  69
  70 val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
  71
  72 val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2
  73
  74 val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list
  75
  76 val compose : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list
  77
  78 val rev_append : 'a1 list -> 'a1 list -> 'a1 list
  79
  80 val reverse : 'a1 list -> 'a1 list
  81
  82 val length : 'a1 list -> Nat.nat
  83
  84 val split_rev :
  85   'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod
  86
  87 val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod
  88
  89 val flatten : 'a1 list list -> 'a1 list
  90
  91 val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1
  92
  93 val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option
  94
  95 val fold :
  96   ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
  97   list -> 'a2
  98
  99 type 'a aop =
 100   'a -> 'a -> 'a
 101   (* singleton inductive, whose constructor was mk_Aop *)
 102
 103 val aop_rect_Type4 :
 104   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
 105
 106 val aop_rect_Type5 :
 107   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
 108
 109 val aop_rect_Type3 :
 110   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
 111
 112 val aop_rect_Type2 :
 113   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
 114
 115 val aop_rect_Type1 :
 116   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
 117
 118 val aop_rect_Type0 :
 119   'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
 120
 121 val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1
 122
 123 val aop_inv_rect_Type4 :
 124   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 125   'a2
 126
 127 val aop_inv_rect_Type3 :
 128   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 129   'a2
 130
 131 val aop_inv_rect_Type2 :
 132   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 133   'a2
 134
 135 val aop_inv_rect_Type1 :
 136   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 137   'a2
 138
 139 val aop_inv_rect_Type0 :
 140   'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 141   'a2
 142
 143 val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __
 144
 145 val dpi1__o__op : 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
 146
 147 val lhd : 'a1 list -> Nat.nat -> 'a1 list
 148
 149 val ltl : 'a1 list -> Nat.nat -> 'a1 list
 150
 151 val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option
 152
 153 val position_of_aux :
 154   ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option
 155
 156 val position_of : ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option
 157
 158 val make_list : 'a1 -> Nat.nat -> 'a1 list
 159