source: driver/extracted/labelledObjects.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 1.1 KB
Line 
1open Preamble
2
3open Setoids
4
5open Monad
6
7open Option
8
9open Div_and_mod
10
11open Jmeq
12
13open Russell
14
15open Util
16
17open Bool
18
19open Relations
20
21open Nat
22
23open Hints_declaration
24
25open Core_notation
26
27open Pts
28
29open Logic
30
31open Types
32
33open List
34
35open Lists
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Positive
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_of : ('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.