extracted/preIdentifiers.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 open Positive
  20
  21 type identifierTag =
  22 | Label
  23 | CostTag
  24 | RegisterTag
  25 | LabelTag
  26 | SymbolTag
  27 | ASMTag
  28
  29 val identifierTag_rect_Type4 :
  30   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
  31
  32 val identifierTag_rect_Type5 :
  33   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
  34
  35 val identifierTag_rect_Type3 :
  36   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
  37
  38 val identifierTag_rect_Type2 :
  39   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
  40
  41 val identifierTag_rect_Type1 :
  42   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
  43
  44 val identifierTag_rect_Type0 :
  45   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1
  46
  47 val identifierTag_inv_rect_Type4 :
  48   identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  49   -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  50
  51 val identifierTag_inv_rect_Type3 :
  52   identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  53   -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  54
  55 val identifierTag_inv_rect_Type2 :
  56   identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  57   -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  58
  59 val identifierTag_inv_rect_Type1 :
  60   identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  61   -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  62
  63 val identifierTag_inv_rect_Type0 :
  64   identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  65   -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  66
  67 val identifierTag_discr : identifierTag -> identifierTag -> __
  68
  69 type identifier =
  70   Positive.pos
  71   (* singleton inductive, whose constructor was an_identifier *)
  72
  73 val identifier_rect_Type4 :
  74   identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
  75
  76 val identifier_rect_Type5 :
  77   identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
  78
  79 val identifier_rect_Type3 :
  80   identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
  81
  82 val identifier_rect_Type2 :
  83   identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
  84
  85 val identifier_rect_Type1 :
  86   identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
  87
  88 val identifier_rect_Type0 :
  89   identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1
  90
  91 val identifier_inv_rect_Type4 :
  92   identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
  93
  94 val identifier_inv_rect_Type3 :
  95   identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
  96
  97 val identifier_inv_rect_Type2 :
  98   identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
  99
 100 val identifier_inv_rect_Type1 :
 101   identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
 102
 103 val identifier_inv_rect_Type0 :
 104   identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1
 105
 106 val identifier_discr : identifierTag -> identifier -> identifier -> __
 107