source: driver/extracted/graphs.ml @ 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 Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Deqsets
14
15open Setoids
16
17open Monad
18
19open Option
20
21open Extranat
22
23open Vector
24
25open Div_and_mod
26
27open Jmeq
28
29open Russell
30
31open List
32
33open Util
34
35open FoldStuff
36
37open Bool
38
39open Relations
40
41open Nat
42
43open BitVector
44
45open BitVectorTrie
46
47open Proper
48
49open PositiveMap
50
51open ErrorMessages
52
53open PreIdentifiers
54
55open Errors
56
57open Extralib
58
59open Lists
60
61open Positive
62
63open Identifiers
64
65open Exp
66
67open Arithmetic
68
69open Integers
70
71open AST
72
73type label = PreIdentifiers.identifier
74
75(** val label_to_ident : label -> AST.ident **)
76let label_to_ident l =
77  let l0 = l in l0
78
79(** val label_eq : label -> label -> (__, __) Types.sum **)
80let label_eq =
81  Identifiers.identifier_eq PreIdentifiers.LabelTag
82
83type 'x graph = 'x Identifiers.identifier_map
84
85(** val graph_fold :
86    (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 graph -> 'a2 -> 'a2 **)
87let graph_fold f graph0 seed =
88  let map = graph0 in PositiveMap.fold f map seed
89
90(** val graph_num_nodes : 'a1 graph -> Nat.nat **)
91let graph_num_nodes g =
92  Identifiers.id_map_size PreIdentifiers.LabelTag g
93
Note: See TracBrowser for help on using the repository browser.