source: extracted/labelledObjects.mli @ 2746

Last change on this file since 2746 was 2649, checked in by sacerdot, 7 years ago

...

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