extracted/labelledObjects.mli

   1 open Preamble
   2
   3 open Setoids
   4
   5 open Monad
   6
   7 open Option
   8
   9 open Div_and_mod
  10
  11 open Jmeq
  12
  13 open Russell
  14
  15 open Util
  16
  17 open Bool
  18
  19 open Relations
  20
  21 open Nat
  22
  23 open Hints_declaration
  24
  25 open Core_notation
  26
  27 open Pts
  28
  29 open Logic
  30
  31 open Types
  32
  33 open List
  34
  35 open Lists
  36
  37 open Proper
  38
  39 open PositiveMap
  40
  41 open Deqsets
  42
  43 open ErrorMessages
  44
  45 open PreIdentifiers
  46
  47 open Errors
  48
  49 open Extralib
  50
  51 open Positive
  52
  53 open Identifiers
  54
  55 type 'a labelled_obj =
  56   (PreIdentifiers.identifier Types.option, 'a) Types.prod
  57
  58 val instruction_matches_identifier :
  59   PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
  60   labelled_obj -> Bool.bool
  61
  62 val does_not_occur :
  63   PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
  64   labelled_obj List.list -> Bool.bool
  65
  66 val occurs_exactly_once :
  67   PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
  68   labelled_obj List.list -> Bool.bool
  69
  70 val index_of_internal :
  71   ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> Nat.nat
  72
  73 val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
  74
  75 val index_of_label :
  76   PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
  77   labelled_obj List.list -> Nat.nat
  78