source: extracted/labelledObjects.mli @ 2729

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

...

File size: 1.1 KB
RevLine 
[2601]1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
[2649]9open ErrorMessages
10
[2601]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
[2649]31open List
32
[2601]33open Lists
34
35open Bool
36
37open Relations
38
39open Nat
40
[2649]41open Positive
[2601]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 :
[2649]59  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
60  labelled_obj -> Bool.bool
[2601]61
62val does_not_occur :
[2649]63  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
64  labelled_obj List.list -> Bool.bool
[2601]65
66val occurs_exactly_once :
[2649]67  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
68  labelled_obj List.list -> Bool.bool
[2601]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 :
[2649]76  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
77  labelled_obj List.list -> Nat.nat
[2601]78
Note: See TracBrowser for help on using the repository browser.