Full development archive
Source code
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (706 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (275 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (112 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (67 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
Global Index
B
Benchmark [library]C
Common [library]Constructive_Undirected_Graph.In_graph_labeled_edge_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.add_edge [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_edge_in_ext [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.edge_label_spec [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.mapsto_edge_equiv_pred [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_remove_edge_edge_succ [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.Add_edge_fail_edge [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.t [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_edge [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_edge_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_labeled_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.VertexMap [module, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.link [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_succ_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_edge_add_edge_2 [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.Edge [module, in Constructive_DigraphInterface]
Constructive_Directed_Graph.vertex_label_spec [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.remove_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.V [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.Add_edge_fail_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_pred_ne [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.mapsto_edge_equiv_pred [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_labeled_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_add_edge_edge [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.EdgeMap [module, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_edge_spec [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_labeled_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_add_edge_weak_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.permute_edge_in [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_edges [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_succ_ne [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_remove_edge_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_pred_spec [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.remove_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_add_edge_weak_edge [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.successors [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_succ [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_edge_add_edge [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.EMapFacts [module, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.vertex_label [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_pred [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_vertex_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.empty_graph [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_succ_ne [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_remove_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.E [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_pred_ne [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_edge_add_edge_2 [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_labeled_vertex_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph [module, in Constructive_DigraphInterface]
Constructive_Directed_Graph.vertex_label [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.remove_edge [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.mapsto_edge_equiv_succ [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_succ_ne_spec [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_edges [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_labeled_edge_spec [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.add_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_vertices_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.link_edge_equiv [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_succ [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.add_edge_w [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_pred_ne_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.VertexMap [module, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_edge_in_ext [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_remove_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_vertex_spec [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.successors [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_remove_edge_edge_pred [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.vertex_label_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_add_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.Add_edge_fail_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.link_edge_equiv [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.V [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_remove_edge_edge_succ [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_ext [definition, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_vertices [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.EdgeMap [module, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.mapsto_edge_equiv_succ [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_add_edge_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_add_edge_weak_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_add_vertex_edge [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.edge_label [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_add_edge_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph [module, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_edge_add_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_remove_edge_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.edge_label [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_add_vertex_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.E [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.add_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.Edge [module, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_add_edge_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_ext [definition, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_remove_edge_edge_pred [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_vertices_spec [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_add_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.VMapFacts [module, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_pred_ne_spec [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.remove_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_edges_spec [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.empty_graph [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.Add_edge_fail_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.add_edge [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_succ_spec [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_pred [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_remove_vertex [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_edges_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.add_edge_w [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.edge_label_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.t [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_remove_edge [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_add_edge_weak_vertex [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.link [axiom, in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_pred_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.VMapFacts [module, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_succ_ne_spec [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_labeled_vertex_spec [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.predecessors [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.predecessors [axiom, in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_labeled_edge [axiom, in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_vertices [axiom, in Constructive_DigraphInterface]
Constructive_Undirected_Graph.EMapFacts [module, in Constructive_UndigraphInterface]
Constructive_DigraphInterface [library]
Constructive_UndigraphInterface [library]
D
D [module, in Benchmark]DigraphInterface [library]
DigraphMapImp [library]
Dijkstra [library]
Directed_GraphMap.In_graph_labeled_edge [definition, in DigraphMapImp]
Directed_GraphMap.link [definition, in DigraphMapImp]
Directed_Graph.V [axiom, in DigraphInterface]
Directed_GraphMap.add_edge_succ_notin [lemma, in DigraphMapImp]
Directed_Graph.EMapFacts [module, in DigraphInterface]
Directed_GraphMap.Make_Graph [constructor, in DigraphMapImp]
Directed_GraphMap.add_edge_pred_notin [lemma, in DigraphMapImp]
Directed_Graph.link [axiom, in DigraphInterface]
Directed_GraphMap.fold_succ_spec [lemma, in DigraphMapImp]
Directed_GraphMap.add_neighborhood_diff [lemma, in DigraphMapImp]
Directed_Edge.edge_eq [lemma, in Directed_edges]
Directed_GraphMap.fold_vertices_spec [lemma, in DigraphMapImp]
Directed_GraphMap.map [projection, in DigraphMapImp]
Directed_GraphMap.In_graph_remove_edge_edge_succ [lemma, in DigraphMapImp]
Directed_Graph.fold_pred [axiom, in DigraphInterface]
Directed_GraphMap.fold_pred_ne [definition, in DigraphMapImp]
Directed_GraphMap.In_graph_labeled_vertex_spec [lemma, in DigraphMapImp]
Directed_Graph.fold_succ [axiom, in DigraphInterface]
Directed_Edge.fst_end [definition, in Directed_edges]
Directed_Edge.incident [definition, in Directed_edges]
Directed_GraphMap.empty_map [definition, in DigraphMapImp]
Directed_GraphMap.In_graph_labeled_edge_weak [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_vertex [definition, in DigraphMapImp]
Directed_Graph.In_graph_labeled_vertex_spec [axiom, in DigraphInterface]
Directed_GraphMap.tt [record, in DigraphMapImp]
Directed_GraphMap.add_vertex_map [definition, in DigraphMapImp]
Directed_GraphMap.In_graph_labeled_edge_spec [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_remove_edge_vertex [lemma, in DigraphMapImp]
Directed_GraphMap.succ_remove_edge_notin [lemma, in DigraphMapImp]
Directed_GraphMap.fold_edges_spec [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_vertex_spec [lemma, in DigraphMapImp]
Directed_GraphMap.fold_vertices [definition, in DigraphMapImp]
Directed_GraphMap.In_add_vertex_edge [lemma, in DigraphMapImp]
Directed_GraphMap.fold_pred [definition, in DigraphMapImp]
Directed_GraphMap.adj_map [definition, in DigraphMapImp]
Directed_GraphMap.fold_succ [definition, in DigraphMapImp]
Directed_Edge.change_fst [lemma, in Directed_edges]
Directed_Graph.fold_succ_ne [axiom, in DigraphInterface]
Directed_GraphMap.add_neighborhood [definition, in DigraphMapImp]
Directed_GraphMap.remove_map_pred_eq [lemma, in DigraphMapImp]
Directed_GraphMap.add_neighborhood_eq [lemma, in DigraphMapImp]
Directed_GraphMap.remove_neighbor_spec [lemma, in DigraphMapImp]
Directed_Edge.snd_end [definition, in Directed_edges]
Directed_GraphMap.remove_map_mapsto [lemma, in DigraphMapImp]
Directed_Graph.In_graph_labeled_edge [axiom, in DigraphInterface]
Directed_GraphMap.remove_edge_map [definition, in DigraphMapImp]
Directed_GraphMap.In_add_vertex [lemma, in DigraphMapImp]
Directed_Graph.E [axiom, in DigraphInterface]
Directed_GraphMap.In_graph_add_edge_weak_edge_2 [lemma, in DigraphMapImp]
Directed_Edge.OTPairFacts [module, in Directed_edges]
Directed_GraphMap.empty_graph [definition, in DigraphMapImp]
Directed_Graph.In_graph_edge_spec [axiom, in DigraphInterface]
Directed_GraphMap.In_graph_add_edge_vertex [lemma, in DigraphMapImp]
Directed_GraphMap.Add_edge_fail_edge [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_add_edge_edge [lemma, in DigraphMapImp]
Directed_GraphMap.pred_succ_add_edge [lemma, in DigraphMapImp]
Directed_Graph.fold_vertices [axiom, in DigraphInterface]
Directed_GraphMap.pred [definition, in DigraphMapImp]
Directed_GraphMap.add_edge_succ [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_edge_spec [lemma, in DigraphMapImp]
Directed_Graph.fold_pred_ne [axiom, in DigraphInterface]
Directed_Graph.vertex_label_spec [axiom, in DigraphInterface]
Directed_GraphMap.empty_graph_empty [lemma, in DigraphMapImp]
Directed_GraphMap.is_pred [definition, in DigraphMapImp]
Directed_Graph.mapsto_edge_equiv_pred [axiom, in DigraphInterface]
Directed_GraphMap.add_edge_map [definition, in DigraphMapImp]
Directed_Graph.In_graph_labeled_edge_spec [axiom, in DigraphInterface]
Directed_GraphMap.EMapFacts [module, in DigraphMapImp]
Directed_Graph.edge_label_spec [axiom, in DigraphInterface]
Directed_GraphMap.pred_succ_add_vertex [lemma, in DigraphMapImp]
Directed_GraphMap.fold_edges [definition, in DigraphMapImp]
Directed_GraphMap.In_remove_edge [lemma, in DigraphMapImp]
Directed_GraphMap.add_neighborhood_comm [lemma, in DigraphMapImp]
Directed_GraphMap.In_remove_vertex [lemma, in DigraphMapImp]
Directed_Graph.edge_label [axiom, in DigraphInterface]
Directed_GraphMap.remove_map_succ_eq [lemma, in DigraphMapImp]
Directed_Graph.In_graph_vertex [axiom, in DigraphInterface]
Directed_Edge.VertexPair [module, in Directed_edges]
Directed_GraphMap.is_succ [definition, in DigraphMapImp]
Directed_GraphMap.mapsto_edge_equiv_pred [lemma, in DigraphMapImp]
Directed_GraphMap.succ_remove_edge_fst [lemma, in DigraphMapImp]
Directed_GraphMap.vertex_label_spec [lemma, in DigraphMapImp]
Directed_GraphMap.remove_map_pred [lemma, in DigraphMapImp]
Directed_GraphMap.succ [definition, in DigraphMapImp]
Directed_GraphMap.Edge [module, in DigraphMapImp]
Directed_Graph.In_graph_labeled_vertex [axiom, in DigraphInterface]
Directed_GraphMap.Equal_remove_empty [lemma, in DigraphMapImp]
Directed_GraphMap.pred_remove_edge [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_edge_add_edge_2 [lemma, in DigraphMapImp]
Directed_GraphMap.remove_map_succ [lemma, in DigraphMapImp]
Directed_GraphMap.V [definition, in DigraphMapImp]
Directed_GraphMap.pred_succ_remove_edge [lemma, in DigraphMapImp]
Directed_Edge.permute [definition, in Directed_edges]
Directed_GraphMap [module, in DigraphMapImp]
Directed_GraphMap.predecessors [definition, in DigraphMapImp]
Directed_Graph.In_graph_edge_in_ext [axiom, in DigraphInterface]
Directed_GraphMap.remove_vertex [definition, in DigraphMapImp]
Directed_GraphMap.In_graph_edge_in_ext [lemma, in DigraphMapImp]
Directed_GraphMap.E [definition, in DigraphMapImp]
Directed_GraphMap.succ_remove_edge [lemma, in DigraphMapImp]
Directed_Graph.fold_succ_spec [axiom, in DigraphInterface]
Directed_Graph.link_edge_equiv [axiom, in DigraphInterface]
Directed_GraphMap.pred_remove_edge_snd [lemma, in DigraphMapImp]
Directed_GraphMap.successors [definition, in DigraphMapImp]
Directed_GraphMap.is_labeled_pred [definition, in DigraphMapImp]
Directed_GraphMap.fold_succ_ne_spec [lemma, in DigraphMapImp]
Directed_GraphMap.add_edge_pred_snd [lemma, in DigraphMapImp]
Directed_GraphMap.add_edge_w [definition, in DigraphMapImp]
Directed_Graph.EdgeMap [module, in DigraphInterface]
Directed_GraphMap.VertexMap [module, in DigraphMapImp]
Directed_GraphMap.In_graph_labeled_vertex [definition, in DigraphMapImp]
Directed_GraphMap.maptype [definition, in DigraphMapImp]
Directed_Graph.fold_edges [axiom, in DigraphInterface]
Directed_Graph.fold_succ_ne_spec [axiom, in DigraphInterface]
Directed_GraphMap.link_edge_equiv [lemma, in DigraphMapImp]
Directed_Edge.OTFacts [module, in Directed_edges]
Directed_Graph.VertexMap [module, in DigraphInterface]
Directed_Graph.VMapFacts [module, in DigraphInterface]
Directed_GraphMap.fold_succ_ne [definition, in DigraphMapImp]
Directed_Graph.fold_edges_spec [axiom, in DigraphInterface]
Directed_Graph.In_graph_edge [axiom, in DigraphInterface]
Directed_GraphMap.is_labeled_succ [definition, in DigraphMapImp]
Directed_Edge [module, in Directed_edges]
Directed_GraphMap.pred_succ_empty [lemma, in DigraphMapImp]
Directed_GraphMap.edge_label [definition, in DigraphMapImp]
Directed_GraphMap.remove_edge [definition, in DigraphMapImp]
Directed_GraphMap.t [definition, in DigraphMapImp]
Directed_GraphMap.unw_pred_succ [lemma, in DigraphMapImp]
Directed_GraphMap.remove_neighbor [definition, in DigraphMapImp]
Directed_Graph.mapsto_edge_equiv_succ [axiom, in DigraphInterface]
Directed_GraphMap.pred_succ [projection, in DigraphMapImp]
Directed_GraphMap.add_edge_pred [lemma, in DigraphMapImp]
Directed_GraphMap.add_edge [definition, in DigraphMapImp]
Directed_Edge.change_snd [lemma, in Directed_edges]
Directed_GraphMap.In_ext_dec [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_edge_add_edge [lemma, in DigraphMapImp]
Directed_Graph.fold_pred_spec [axiom, in DigraphInterface]
Directed_GraphMap.In_graph_add_edge_weak_edge [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_remove_edge_edge_pred [lemma, in DigraphMapImp]
Directed_Graph.predecessors [axiom, in DigraphInterface]
Directed_GraphMap.fold_pred_ne_spec [lemma, in DigraphMapImp]
Directed_GraphMap.fold_pred_spec [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_edge [definition, in DigraphMapImp]
Directed_Graph.In_graph_vertex_spec [axiom, in DigraphInterface]
Directed_GraphMap.add_neighborhood_compat [lemma, in DigraphMapImp]
Directed_GraphMap.remove_map [definition, in DigraphMapImp]
Directed_Graph.fold_vertices_spec [axiom, in DigraphInterface]
Directed_Graph.t [axiom, in DigraphInterface]
Directed_GraphMap.Add_edge_fail_vertex [lemma, in DigraphMapImp]
Directed_GraphMap.add_vertex [definition, in DigraphMapImp]
Directed_GraphMap.VMapFacts [module, in DigraphMapImp]
Directed_GraphMap.EdgeMap [module, in DigraphMapImp]
Directed_Graph [module, in DigraphInterface]
Directed_Graph.vertex_label [axiom, in DigraphInterface]
Directed_GraphMap.pred_remove_edge_notin [lemma, in DigraphMapImp]
Directed_GraphMap.In_graph_add_edge_weak_vertex [lemma, in DigraphMapImp]
Directed_Graph.fold_pred_ne_spec [axiom, in DigraphInterface]
Directed_GraphMap.mapsto_edge_equiv_succ [lemma, in DigraphMapImp]
Directed_GraphMap.pred_succ_remove_vertex [lemma, in DigraphMapImp]
Directed_GraphMap.add_edge_succ_fst [lemma, in DigraphMapImp]
Directed_Edge.incident_dec [lemma, in Directed_edges]
Directed_GraphMap.add_neighborhood_spec [lemma, in DigraphMapImp]
Directed_GraphMap.edge_label_spec [lemma, in DigraphMapImp]
Directed_Graph.successors [axiom, in DigraphInterface]
Directed_GraphMap.vertex_label [definition, in DigraphMapImp]
Directed_GraphMap.In_ext [definition, in DigraphMapImp]
Directed_Graph.Edge [module, in DigraphInterface]
Directed_edges [library]
E
Eadd [module, in Common]Eadd.add_elements_cons [lemma, in Common]
Eadd.eqlistA_fold [lemma, in Common]
Eadd.NoDup_sorted_add_cons [lemma, in Common]
Eadd.NoDup_sorted_equiv_eq [lemma, in Common]
eqlistAFacts [module, in Common]
eqlistAFacts.eqlistA_trans [lemma, in Common]
eqlistAFacts.eqlistA_refl [lemma, in Common]
eqlistAFacts.eqlistA_sym [lemma, in Common]
Extraction [library]
G
G [module, in Benchmark]GraphProps [module, in Graph_Properties]
GraphProps.eq [definition, in Graph_Properties]
GraphProps.eq_sym [lemma, in Graph_Properties]
GraphProps.eq_trans [lemma, in Graph_Properties]
GraphProps.eq_refl [lemma, in Graph_Properties]
GraphProps.In_graph_labeled_vertex_eq [lemma, in Graph_Properties]
GraphProps.In_graph_vertex_dec [lemma, in Graph_Properties]
GraphProps.In_graph_labeled_edge_weak [lemma, in Graph_Properties]
GraphProps.In_graph_labeled_vertex_weak [lemma, in Graph_Properties]
GraphProps.In_graph_labeled_edge_eq [lemma, in Graph_Properties]
GraphProps.In_graph_edge_dec [lemma, in Graph_Properties]
GraphProps.In_graph_edge_strong [lemma, in Graph_Properties]
GraphProps.In_graph_vertex_strong [lemma, in Graph_Properties]
GraphProps.labeled_edge_edge_label [lemma, in Graph_Properties]
GraphProps.labeled_vertex_vertex_label [lemma, in Graph_Properties]
_ =G _ [notation, in Graph_Properties]
Graph_Properties [library]
L
Labels [module, in Labels]Labels [library]
Labels.EdgeLabel [axiom, in Labels]
Labels.NodeLabel [axiom, in Labels]
M
MapFacts [library]MyMapFacts [module, in MapFacts]
MyMapFacts.add_add_Eq [lemma, in MapFacts]
MyMapFacts.associative_fold_maps [section, in MapFacts]
MyMapFacts.associative_fold_maps.eqA_refl [variable, in MapFacts]
MyMapFacts.associative_fold_maps.eqA_trans [variable, in MapFacts]
MyMapFacts.associative_fold_maps.B [variable, in MapFacts]
MyMapFacts.associative_fold_maps.eqA [variable, in MapFacts]
MyMapFacts.associative_fold_maps.A [variable, in MapFacts]
MyMapFacts.EqualMap [definition, in MapFacts]
MyMapFacts.EqualMap_trans [lemma, in MapFacts]
MyMapFacts.EqualMap_refl [lemma, in MapFacts]
MyMapFacts.eq_map_option [inductive, in MapFacts]
MyMapFacts.fold_invariant2 [lemma, in MapFacts]
MyMapFacts.fold_left_assoc_map [lemma, in MapFacts]
MyMapFacts.fold_left_assoc [lemma, in MapFacts]
MyMapFacts.fold_left_assoc_map_find_nodup [lemma, in MapFacts]
MyMapFacts.fold_left_compat [lemma, in MapFacts]
MyMapFacts.fold_invariant [lemma, in MapFacts]
MyMapFacts.fold_invariant_cons [lemma, in MapFacts]
MyMapFacts.general_associative_fold.B [variable, in MapFacts]
MyMapFacts.general_associative_fold.eqA_refl [variable, in MapFacts]
MyMapFacts.general_associative_fold.eqA [variable, in MapFacts]
MyMapFacts.general_associative_fold.eqA_trans [variable, in MapFacts]
MyMapFacts.general_associative_fold.A [variable, in MapFacts]
MyMapFacts.general_associative_fold.eqB [variable, in MapFacts]
MyMapFacts.general_associative_fold [section, in MapFacts]
MyMapFacts.In_MapsTo [lemma, in MapFacts]
MyMapFacts.MapFacts [module, in MapFacts]
MyMapFacts.MapsTo_In [lemma, in MapFacts]
MyMapFacts.MapsTo_In.A [variable, in MapFacts]
MyMapFacts.MapsTo_In [section, in MapFacts]
MyMapFacts.Mapsto_In [lemma, in MapFacts]
MyMapFacts.None_eq [constructor, in MapFacts]
MyMapFacts.Some_eq [constructor, in MapFacts]
MyMapFacts.SubMap [definition, in MapFacts]
MyMapFacts.Submap [section, in MapFacts]
MyMapFacts.Submap.A [variable, in MapFacts]
N
Nat_Labels [module, in Labels]Nat_Labels.NodeLabel [definition, in Labels]
Nat_Labels.EdgeLabel [definition, in Labels]
P
Path [module, in Paths]Paths [library]
Path.cut_path [lemma, in Paths]
Path.cut_path_aux [lemma, in Paths]
Path.decompose_app [lemma, in Paths]
Path.eval [definition, in Paths]
Path.In_graph_edge_equiv [lemma, in Paths]
Path.in_path_in_graph [lemma, in Paths]
Path.minus_plus_plus_minus [lemma, in Paths]
Path.P [module, in Paths]
Path.path [inductive, in Paths]
Path.path_edge_charac [lemma, in Paths]
Path.path_end [lemma, in Paths]
Path.path_value_eq [lemma, in Paths]
Path.path_snd_ext [lemma, in Paths]
Path.path_trans [lemma, in Paths]
Path.path_eqlistA [lemma, in Paths]
Path.path_shorten_1 [lemma, in Paths]
Path.path_ends_in_graph [lemma, in Paths]
Path.path_nil_eq_end [lemma, in Paths]
Path.path_shorten_2 [lemma, in Paths]
Path.path_value_ge_edge [lemma, in Paths]
Path.path_post [constructor, in Paths]
Path.path_self [constructor, in Paths]
Path.pos_edge_pos_path [lemma, in Paths]
S
Shortest_path.remove_remove_cp [lemma, in Dijkstra]Shortest_path.EdgeList [module, in Dijkstra]
Shortest_path.path_init [lemma, in Dijkstra]
Shortest_path.nonoptimal_vertices_nb [definition, in Dijkstra]
Shortest_path.pathmap [record, in Dijkstra]
Shortest_path.null_init_3 [lemma, in Dijkstra]
Shortest_path.CoupleSet [module, in Dijkstra]
Shortest_path.update_closed_inv [lemma, in Dijkstra]
Shortest_path.update_list_neq_aux [lemma, in Dijkstra]
Shortest_path.map [projection, in Dijkstra]
Shortest_path.EA [module, in Dijkstra]
Shortest_path.open_vertices_nb_eq [lemma, in Dijkstra]
Shortest_path.status [inductive, in Dijkstra]
Shortest_path.set_open_init [lemma, in Dijkstra]
Shortest_path.init [definition, in Dijkstra]
Shortest_path.path_implies_reachable [lemma, in Dijkstra]
Shortest_path.list_as_OT.lt_not_eq [lemma, in Dijkstra]
Shortest_path.Dijkstra_optimal [lemma, in Dijkstra]
Shortest_path.null_init [definition, in Dijkstra]
Shortest_path.update [definition, in Dijkstra]
Shortest_path.Reached [constructor, in Dijkstra]
Shortest_path.init_finite [lemma, in Dijkstra]
Shortest_path.update_list_eq [lemma, in Dijkstra]
Shortest_path.Dijkstra_root [lemma, in Dijkstra]
Shortest_path.Unreached [constructor, in Dijkstra]
Shortest_path.Dijkstra_measure [definition, in Dijkstra]
Shortest_path.consistant_status [lemma, in Dijkstra]
Shortest_path.add_cp [lemma, in Dijkstra]
Shortest_path.nonoptimal_vertices_nb_eq_unreached [lemma, in Dijkstra]
Shortest_path.infinite_none_no_open [lemma, in Dijkstra]
Shortest_path.Couple [module, in Dijkstra]
Shortest_path.root_find_init [lemma, in Dijkstra]
Shortest_path.in_map_in_graph [projection, in Dijkstra]
Shortest_path.completeness_2 [lemma, in Dijkstra]
Shortest_path.set_open_iter [lemma, in Dijkstra]
Shortest_path.Dijkstra_graph [lemma, in Dijkstra]
Shortest_path.equivalence_eq_key [lemma, in Dijkstra]
Shortest_path.Open [constructor, in Dijkstra]
Shortest_path.iteration_pathmap [definition, in Dijkstra]
Shortest_path.shortest [projection, in Dijkstra]
Shortest_path.find_min_2 [lemma, in Dijkstra]
Shortest_path.add_remove_cp [lemma, in Dijkstra]
Shortest_path.path_construction [lemma, in Dijkstra]
Shortest_path.completeness [lemma, in Dijkstra]
Shortest_path.Dijkstra [definition, in Dijkstra]
Shortest_path.graph [projection, in Dijkstra]
Shortest_path.in_map_in_graph_init [lemma, in Dijkstra]
Shortest_path.list_as_OT.ltcons [constructor, in Dijkstra]
Shortest_path.list_as_OT.eq_trans [lemma, in Dijkstra]
Shortest_path.list_as_OT.lt_trans [lemma, in Dijkstra]
Shortest_path.list_as_OT.eq_dec [lemma, in Dijkstra]
Shortest_path.list_as_OT.eq_sym [lemma, in Dijkstra]
Shortest_path.root_find [projection, in Dijkstra]
Shortest_path.Optimal [constructor, in Dijkstra]
Shortest_path.correctness_aux [lemma, in Dijkstra]
Shortest_path.dynamic [projection, in Dijkstra]
Shortest_path.shortest_init [lemma, in Dijkstra]
Shortest_path.Dijkstra_graph_aux [lemma, in Dijkstra]
Shortest_path.list_as_OT.lt_ [inductive, in Dijkstra]
Shortest_path.first_iter_charac [lemma, in Dijkstra]
Shortest_path.Dijkstra_root_aux [lemma, in Dijkstra]
Shortest_path.set [projection, in Dijkstra]
Shortest_path.list_as_OT.eq [definition, in Dijkstra]
Shortest_path.first_iter [definition, in Dijkstra]
Shortest_path.PS [module, in Dijkstra]
Shortest_path.Couple_ [module, in Dijkstra]
Shortest_path.nonoptimal_vertices_nb_eq_up [lemma, in Dijkstra]
Shortest_path.Make_pathmap [constructor, in Dijkstra]
Shortest_path.eqlistAF [module, in Dijkstra]
Shortest_path.set_open [projection, in Dijkstra]
Shortest_path.list_as_OT.eq_refl [lemma, in Dijkstra]
Shortest_path.shortest_iteration [lemma, in Dijkstra]
Shortest_path.shortest_path_length [definition, in Dijkstra]
Shortest_path.list_as_OT [module, in Dijkstra]
Shortest_path.iteration [definition, in Dijkstra]
Shortest_path.list_as_OT.OP [module, in Dijkstra]
Shortest_path.root [projection, in Dijkstra]
Shortest_path.iteration_pathmap_none [lemma, in Dijkstra]
Shortest_path.find_min_none_charac [lemma, in Dijkstra]
Shortest_path.iteration_root [lemma, in Dijkstra]
Shortest_path.dynamic_continuation [lemma, in Dijkstra]
Shortest_path.list_as_OT.lt_tail [constructor, in Dijkstra]
Shortest_path.list_as_OT.compare [lemma, in Dijkstra]
Shortest_path.shortest_path [definition, in Dijkstra]
Shortest_path.equiv_edge_eq [definition, in Dijkstra]
Shortest_path.null_init_1 [lemma, in Dijkstra]
Shortest_path.root_find_iter [lemma, in Dijkstra]
Shortest_path.add_add_cp [lemma, in Dijkstra]
Shortest_path.list_as_OT.lt [definition, in Dijkstra]
Shortest_path.path_iteration [lemma, in Dijkstra]
Shortest_path.is_path [projection, in Dijkstra]
Shortest_path.iteration_graph [lemma, in Dijkstra]
Shortest_path.dynamic_init [lemma, in Dijkstra]
Shortest_path.null_init_2 [lemma, in Dijkstra]
Shortest_path.first_iter_not_opt [lemma, in Dijkstra]
Shortest_path.dynamic_prog [definition, in Dijkstra]
Shortest_path.correctness [lemma, in Dijkstra]
Shortest_path.update_list [definition, in Dijkstra]
Shortest_path.find_min_1 [lemma, in Dijkstra]
Shortest_path.iteration_finite [lemma, in Dijkstra]
Shortest_path [module, in Dijkstra]
Shortest_path.list_as_OT.ltnil [constructor, in Dijkstra]
Shortest_path.P [module, in Dijkstra]
Shortest_path.correct_path [definition, in Dijkstra]
Shortest_path.vertex_status [inductive, in Dijkstra]
Shortest_path.list_as_OT.t [definition, in Dijkstra]
Shortest_path.dynamic_iteration [lemma, in Dijkstra]
Shortest_path.update_list_neq [lemma, in Dijkstra]
Shortest_path.in_map_in_graph_iter [lemma, in Dijkstra]
Shortest_path.iteration_closed_charac [lemma, in Dijkstra]
Shortest_path.PPS [module, in Dijkstra]
Shortest_path.Dijkstra_path [lemma, in Dijkstra]
Shortest_path.init_dijkstra [definition, in Dijkstra]
Shortest_path.first_iter_charac_2 [lemma, in Dijkstra]
Shortest_path.find_min_opt [lemma, in Dijkstra]
Shortest_path.find_min [definition, in Dijkstra]
Shortest_path.update_list_eq_aux [lemma, in Dijkstra]
Shortest_path.remove_cp [lemma, in Dijkstra]
U
UDSpec [module, in Unlabeled_spec]UDSpec.Add_edge_fail_vertex_u [lemma, in Unlabeled_spec]
UDSpec.Add_edge_fail_edge_u [lemma, in Unlabeled_spec]
UDSpec.In_add_vertex_edge_u [lemma, in Unlabeled_spec]
UDSpec.In_add_vertex_u [lemma, in Unlabeled_spec]
UDSpec.In_remove_vertex_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_remove_edge_vertex_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_remove_edge_edge_pred_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_add_edge_weak_vertex_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_add_edge_weak_edge_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_edge_add_edge_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_remove_edge_edge_succ_u [lemma, in Unlabeled_spec]
UDSpec.In_remove_edge_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_add_edge_edge_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_add_edge_vertex_u [lemma, in Unlabeled_spec]
UDSpec.In_graph_edge_add_edge_2_u [lemma, in Unlabeled_spec]
UDSpec.Props [module, in Unlabeled_spec]
UndigraphInterface [library]
UndigraphMapImp [library]
Undirected_Graph [module, in UndigraphInterface]
Undirected_GraphMap.adj_remove_edge [lemma, in UndigraphMapImp]
Undirected_Graph.In_graph_edge_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.empty_graph_empty [lemma, in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge_in_ext [lemma, in UndigraphMapImp]
Undirected_GraphMap.mapsto_edge_equiv_pred [lemma, in UndigraphMapImp]
Undirected_Graph.fold_edges_spec [axiom, in UndigraphInterface]
Undirected_Graph.fold_succ_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.adj [definition, in UndigraphMapImp]
Undirected_Graph.fold_pred_ne_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.fold_vertices [definition, in UndigraphMapImp]
Undirected_Graph.In_graph_labeled_vertex [axiom, in UndigraphInterface]
Undirected_GraphMap.In_graph_add_edge_edge [lemma, in UndigraphMapImp]
Undirected_Graph.fold_edges [axiom, in UndigraphInterface]
Undirected_GraphMap.predecessors [definition, in UndigraphMapImp]
Undirected_GraphMap.mapsto_edge_equiv_succ [lemma, in UndigraphMapImp]
Undirected_GraphMap.adjacency_add_vertex [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_diff [lemma, in UndigraphMapImp]
Undirected_GraphMap.adj_remove_edge_fst [lemma, in UndigraphMapImp]
Undirected_GraphMap.remove_vertex [definition, in UndigraphMapImp]
Undirected_GraphMap.remove_map [definition, in UndigraphMapImp]
Undirected_GraphMap.pred [definition, in UndigraphMapImp]
Undirected_GraphMap.In_graph_remove_edge_edge_pred [lemma, in UndigraphMapImp]
Undirected_GraphMap.maptype [definition, in UndigraphMapImp]
Undirected_GraphMap.adjacency_remove_edge [lemma, in UndigraphMapImp]
Undirected_Graph.t [axiom, in UndigraphInterface]
Undirected_GraphMap.remove_neighbor_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.In_graph_remove_edge_edge_succ [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood [definition, in UndigraphMapImp]
Undirected_GraphMap.remove_map_adj_eq [lemma, in UndigraphMapImp]
Undirected_GraphMap.In_graph_vertex [definition, in UndigraphMapImp]
Undirected_GraphMap.In_ext [definition, in UndigraphMapImp]
Undirected_GraphMap.adjacent [definition, in UndigraphMapImp]
Undirected_GraphMap.successors [definition, in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge_add_edge [lemma, in UndigraphMapImp]
Undirected_Graph.E [axiom, in UndigraphInterface]
Undirected_Graph.edge_label [axiom, in UndigraphInterface]
Undirected_GraphMap.In_ext_dec [lemma, in UndigraphMapImp]
Undirected_GraphMap.remove_neighbor [definition, in UndigraphMapImp]
Undirected_GraphMap.In_graph_add_edge_vertex [lemma, in UndigraphMapImp]
Undirected_GraphMap.V [definition, in UndigraphMapImp]
Undirected_GraphMap.Equal_remove_empty [lemma, in UndigraphMapImp]
Undirected_Graph.permute_edge_in [axiom, in UndigraphInterface]
Undirected_Graph.fold_vertices_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.fold_pred [definition, in UndigraphMapImp]
Undirected_GraphMap.adjacency_remove_vertex [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_spec [lemma, in UndigraphMapImp]
Undirected_Graph.mapsto_edge_equiv_succ [axiom, in UndigraphInterface]
Undirected_GraphMap.Edge [module, in UndigraphMapImp]
Undirected_GraphMap.edge_label [definition, in UndigraphMapImp]
Undirected_GraphMap.In_graph_remove_edge_vertex [lemma, in UndigraphMapImp]
Undirected_Graph.mapsto_edge_equiv_pred [axiom, in UndigraphInterface]
Undirected_Graph.fold_succ_ne [axiom, in UndigraphInterface]
Undirected_Graph.In_graph_vertex_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.add_edge [definition, in UndigraphMapImp]
Undirected_GraphMap.In_graph_labeled_edge_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.link [definition, in UndigraphMapImp]
Undirected_Graph.In_graph_edge_in_ext [axiom, in UndigraphInterface]
Undirected_Graph.EdgeMap [module, in UndigraphInterface]
Undirected_Graph.V [axiom, in UndigraphInterface]
Undirected_GraphMap.In_graph_add_edge_weak_vertex [lemma, in UndigraphMapImp]
Undirected_Graph.VMapFacts [module, in UndigraphInterface]
Undirected_GraphMap.adjacency_add_edge [lemma, in UndigraphMapImp]
Undirected_GraphMap.is_labeled_adj [definition, in UndigraphMapImp]
Undirected_GraphMap.add_edge_adj [lemma, in UndigraphMapImp]
Undirected_GraphMap.fold_succ_ne [definition, in UndigraphMapImp]
Undirected_GraphMap.adjacency [projection, in UndigraphMapImp]
Undirected_GraphMap.In_remove_vertex [lemma, in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge [definition, in UndigraphMapImp]
Undirected_GraphMap.edge_label_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_edge_adj_snd [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_edge_w [definition, in UndigraphMapImp]
Undirected_GraphMap.Mapsto_In [lemma, in UndigraphMapImp]
Undirected_Graph.fold_vertices [axiom, in UndigraphInterface]
Undirected_GraphMap.EdgeMap [module, in UndigraphMapImp]
Undirected_GraphMap.add_edge_adj_fst [lemma, in UndigraphMapImp]
Undirected_GraphMap.VMapFacts [module, in UndigraphMapImp]
Undirected_GraphMap.EMapsto_In [lemma, in UndigraphMapImp]
Undirected_GraphMap.t [definition, in UndigraphMapImp]
Undirected_Graph.In_graph_labeled_edge_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.fold_pred_ne [definition, in UndigraphMapImp]
Undirected_GraphMap.Add_edge_fail_edge [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_vertex [definition, in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.fold_succ_ne_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.adjacency_empty [lemma, in UndigraphMapImp]
Undirected_GraphMap.adj_remove_edge_notin [lemma, in UndigraphMapImp]
Undirected_Graph.fold_pred [axiom, in UndigraphInterface]
Undirected_Graph.EMapFacts [module, in UndigraphInterface]
Undirected_GraphMap.fold_succ [definition, in UndigraphMapImp]
Undirected_Graph.link_edge_equiv [axiom, in UndigraphInterface]
Undirected_GraphMap.Add_edge_fail_vertex [lemma, in UndigraphMapImp]
Undirected_Graph.Edge [module, in UndigraphInterface]
Undirected_GraphMap.EMapFacts [module, in UndigraphMapImp]
Undirected_Graph.In_graph_labeled_edge [axiom, in UndigraphInterface]
Undirected_GraphMap.remove_edge_map [definition, in UndigraphMapImp]
Undirected_Graph.predecessors [axiom, in UndigraphInterface]
Undirected_GraphMap.add_neighborhood_eq [lemma, in UndigraphMapImp]
Undirected_GraphMap.tt [record, in UndigraphMapImp]
Undirected_GraphMap.remove_map_mapsto [lemma, in UndigraphMapImp]
Undirected_GraphMap.empty_map [definition, in UndigraphMapImp]
Undirected_Graph.vertex_label [axiom, in UndigraphInterface]
Undirected_GraphMap.vertex_label [definition, in UndigraphMapImp]
Undirected_GraphMap.map [projection, in UndigraphMapImp]
Undirected_GraphMap.add_vertex_map [definition, in UndigraphMapImp]
Undirected_GraphMap.fold_edges_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.succ [definition, in UndigraphMapImp]
Undirected_GraphMap.empty_graph [definition, in UndigraphMapImp]
Undirected_GraphMap.fold_vertices_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.adj_remove_edge_snd [lemma, in UndigraphMapImp]
Undirected_Graph.fold_pred_ne [axiom, in UndigraphInterface]
Undirected_GraphMap.Make_Graph [constructor, in UndigraphMapImp]
Undirected_GraphMap.In_graph_labeled_vertex_spec [lemma, in UndigraphMapImp]
Undirected_Graph.vertex_label_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.In_graph_vertex_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_edge_adj_notin [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_compat [lemma, in UndigraphMapImp]
Undirected_Graph.In_graph_edge [axiom, in UndigraphInterface]
Undirected_Graph.link [axiom, in UndigraphInterface]
Undirected_Graph.fold_succ_ne_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.vertex_label_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.E [definition, in UndigraphMapImp]
Undirected_GraphMap.unw_adjacency [lemma, in UndigraphMapImp]
Undirected_GraphMap.In_add_vertex [lemma, in UndigraphMapImp]
Undirected_GraphMap.fold_pred_ne_spec [lemma, in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_comm [lemma, in UndigraphMapImp]
Undirected_Graph.fold_succ [axiom, in UndigraphInterface]
Undirected_GraphMap.adj_map [definition, in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge_add_edge_2 [lemma, in UndigraphMapImp]
Undirected_GraphMap.remove_edge [definition, in UndigraphMapImp]
Undirected_GraphMap.In_add_vertex_edge [lemma, in UndigraphMapImp]
Undirected_Graph.fold_pred_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.In_remove_edge [lemma, in UndigraphMapImp]
Undirected_GraphMap.In_graph_labeled_edge [definition, in UndigraphMapImp]
Undirected_GraphMap.link_edge_equiv [lemma, in UndigraphMapImp]
Undirected_GraphMap [module, in UndigraphMapImp]
Undirected_GraphMap.In_graph_add_edge_weak_edge [lemma, in UndigraphMapImp]
Undirected_Graph.VertexMap [module, in UndigraphInterface]
Undirected_GraphMap.fold_edges [definition, in UndigraphMapImp]
Undirected_GraphMap.fold_succ_spec [lemma, in UndigraphMapImp]
Undirected_Graph.successors [axiom, in UndigraphInterface]
Undirected_GraphMap.remove_map_adj [lemma, in UndigraphMapImp]
Undirected_GraphMap.fold_pred_spec [lemma, in UndigraphMapImp]
Undirected_Graph.edge_label_spec [axiom, in UndigraphInterface]
Undirected_Graph.In_graph_vertex [axiom, in UndigraphInterface]
Undirected_GraphMap.In_graph_labeled_vertex [definition, in UndigraphMapImp]
Undirected_GraphMap.is_adj [definition, in UndigraphMapImp]
Undirected_GraphMap.permute_edge_in [lemma, in UndigraphMapImp]
Undirected_Graph.In_graph_labeled_vertex_spec [axiom, in UndigraphInterface]
Undirected_GraphMap.add_edge_map [definition, in UndigraphMapImp]
Undirected_GraphMap.VertexMap [module, in UndigraphMapImp]
Undirected_GraphMap.In_graph_add_edge_weak_edge_2 [lemma, in UndigraphMapImp]
Unlabeled_spec [library]
UUSpec [module, in Unlabeled_spec]
UUSpec.Add_edge_fail_vertex_u [lemma, in Unlabeled_spec]
UUSpec.Add_edge_fail_edge_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_remove_edge_vertex_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_remove_edge_edge_pred_u [lemma, in Unlabeled_spec]
UUSpec.In_remove_edge_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_add_edge_vertex_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_add_edge_edge_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_edge_add_edge_2_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_remove_edge_edge_succ_u [lemma, in Unlabeled_spec]
UUSpec.In_add_vertex_edge_u [lemma, in Unlabeled_spec]
UUSpec.In_add_vertex_u [lemma, in Unlabeled_spec]
UUSpec.In_remove_vertex_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_add_edge_weak_vertex_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_edge_add_edge_u [lemma, in Unlabeled_spec]
UUSpec.In_graph_add_edge_weak_edge_u [lemma, in Unlabeled_spec]
UUSpec.Props [module, in Unlabeled_spec]
Projection Index
D
Directed_GraphMap.map [in DigraphMapImp]Directed_GraphMap.pred_succ [in DigraphMapImp]
S
Shortest_path.map [in Dijkstra]Shortest_path.in_map_in_graph [in Dijkstra]
Shortest_path.shortest [in Dijkstra]
Shortest_path.graph [in Dijkstra]
Shortest_path.root_find [in Dijkstra]
Shortest_path.dynamic [in Dijkstra]
Shortest_path.set [in Dijkstra]
Shortest_path.set_open [in Dijkstra]
Shortest_path.root [in Dijkstra]
Shortest_path.is_path [in Dijkstra]
U
Undirected_GraphMap.adjacency [in UndigraphMapImp]Undirected_GraphMap.map [in UndigraphMapImp]
Record Index
D
Directed_GraphMap.tt [in DigraphMapImp]S
Shortest_path.pathmap [in Dijkstra]U
Undirected_GraphMap.tt [in UndigraphMapImp]Lemma Index
D
Directed_GraphMap.add_edge_succ_notin [in DigraphMapImp]Directed_GraphMap.add_edge_pred_notin [in DigraphMapImp]
Directed_GraphMap.fold_succ_spec [in DigraphMapImp]
Directed_GraphMap.add_neighborhood_diff [in DigraphMapImp]
Directed_Edge.edge_eq [in Directed_edges]
Directed_GraphMap.fold_vertices_spec [in DigraphMapImp]
Directed_GraphMap.In_graph_remove_edge_edge_succ [in DigraphMapImp]
Directed_GraphMap.In_graph_labeled_vertex_spec [in DigraphMapImp]
Directed_GraphMap.In_graph_labeled_edge_weak [in DigraphMapImp]
Directed_GraphMap.In_graph_labeled_edge_spec [in DigraphMapImp]
Directed_GraphMap.In_graph_remove_edge_vertex [in DigraphMapImp]
Directed_GraphMap.succ_remove_edge_notin [in DigraphMapImp]
Directed_GraphMap.fold_edges_spec [in DigraphMapImp]
Directed_GraphMap.In_graph_vertex_spec [in DigraphMapImp]
Directed_GraphMap.In_add_vertex_edge [in DigraphMapImp]
Directed_Edge.change_fst [in Directed_edges]
Directed_GraphMap.remove_map_pred_eq [in DigraphMapImp]
Directed_GraphMap.add_neighborhood_eq [in DigraphMapImp]
Directed_GraphMap.remove_neighbor_spec [in DigraphMapImp]
Directed_GraphMap.remove_map_mapsto [in DigraphMapImp]
Directed_GraphMap.In_add_vertex [in DigraphMapImp]
Directed_GraphMap.In_graph_add_edge_weak_edge_2 [in DigraphMapImp]
Directed_GraphMap.In_graph_add_edge_vertex [in DigraphMapImp]
Directed_GraphMap.Add_edge_fail_edge [in DigraphMapImp]
Directed_GraphMap.In_graph_add_edge_edge [in DigraphMapImp]
Directed_GraphMap.pred_succ_add_edge [in DigraphMapImp]
Directed_GraphMap.add_edge_succ [in DigraphMapImp]
Directed_GraphMap.In_graph_edge_spec [in DigraphMapImp]
Directed_GraphMap.empty_graph_empty [in DigraphMapImp]
Directed_GraphMap.pred_succ_add_vertex [in DigraphMapImp]
Directed_GraphMap.In_remove_edge [in DigraphMapImp]
Directed_GraphMap.add_neighborhood_comm [in DigraphMapImp]
Directed_GraphMap.In_remove_vertex [in DigraphMapImp]
Directed_GraphMap.remove_map_succ_eq [in DigraphMapImp]
Directed_GraphMap.mapsto_edge_equiv_pred [in DigraphMapImp]
Directed_GraphMap.succ_remove_edge_fst [in DigraphMapImp]
Directed_GraphMap.vertex_label_spec [in DigraphMapImp]
Directed_GraphMap.remove_map_pred [in DigraphMapImp]
Directed_GraphMap.Equal_remove_empty [in DigraphMapImp]
Directed_GraphMap.pred_remove_edge [in DigraphMapImp]
Directed_GraphMap.In_graph_edge_add_edge_2 [in DigraphMapImp]
Directed_GraphMap.remove_map_succ [in DigraphMapImp]
Directed_GraphMap.pred_succ_remove_edge [in DigraphMapImp]
Directed_GraphMap.In_graph_edge_in_ext [in DigraphMapImp]
Directed_GraphMap.succ_remove_edge [in DigraphMapImp]
Directed_GraphMap.pred_remove_edge_snd [in DigraphMapImp]
Directed_GraphMap.fold_succ_ne_spec [in DigraphMapImp]
Directed_GraphMap.add_edge_pred_snd [in DigraphMapImp]
Directed_GraphMap.link_edge_equiv [in DigraphMapImp]
Directed_GraphMap.pred_succ_empty [in DigraphMapImp]
Directed_GraphMap.unw_pred_succ [in DigraphMapImp]
Directed_GraphMap.add_edge_pred [in DigraphMapImp]
Directed_Edge.change_snd [in Directed_edges]
Directed_GraphMap.In_ext_dec [in DigraphMapImp]
Directed_GraphMap.In_graph_edge_add_edge [in DigraphMapImp]
Directed_GraphMap.In_graph_add_edge_weak_edge [in DigraphMapImp]
Directed_GraphMap.In_graph_remove_edge_edge_pred [in DigraphMapImp]
Directed_GraphMap.fold_pred_ne_spec [in DigraphMapImp]
Directed_GraphMap.fold_pred_spec [in DigraphMapImp]
Directed_GraphMap.add_neighborhood_compat [in DigraphMapImp]
Directed_GraphMap.Add_edge_fail_vertex [in DigraphMapImp]
Directed_GraphMap.pred_remove_edge_notin [in DigraphMapImp]
Directed_GraphMap.In_graph_add_edge_weak_vertex [in DigraphMapImp]
Directed_GraphMap.mapsto_edge_equiv_succ [in DigraphMapImp]
Directed_GraphMap.pred_succ_remove_vertex [in DigraphMapImp]
Directed_GraphMap.add_edge_succ_fst [in DigraphMapImp]
Directed_Edge.incident_dec [in Directed_edges]
Directed_GraphMap.add_neighborhood_spec [in DigraphMapImp]
Directed_GraphMap.edge_label_spec [in DigraphMapImp]
E
Eadd.add_elements_cons [in Common]Eadd.eqlistA_fold [in Common]
Eadd.NoDup_sorted_add_cons [in Common]
Eadd.NoDup_sorted_equiv_eq [in Common]
eqlistAFacts.eqlistA_trans [in Common]
eqlistAFacts.eqlistA_refl [in Common]
eqlistAFacts.eqlistA_sym [in Common]
G
GraphProps.eq_sym [in Graph_Properties]GraphProps.eq_trans [in Graph_Properties]
GraphProps.eq_refl [in Graph_Properties]
GraphProps.In_graph_labeled_vertex_eq [in Graph_Properties]
GraphProps.In_graph_vertex_dec [in Graph_Properties]
GraphProps.In_graph_labeled_edge_weak [in Graph_Properties]
GraphProps.In_graph_labeled_vertex_weak [in Graph_Properties]
GraphProps.In_graph_labeled_edge_eq [in Graph_Properties]
GraphProps.In_graph_edge_dec [in Graph_Properties]
GraphProps.In_graph_edge_strong [in Graph_Properties]
GraphProps.In_graph_vertex_strong [in Graph_Properties]
GraphProps.labeled_edge_edge_label [in Graph_Properties]
GraphProps.labeled_vertex_vertex_label [in Graph_Properties]
M
MyMapFacts.add_add_Eq [in MapFacts]MyMapFacts.EqualMap_trans [in MapFacts]
MyMapFacts.EqualMap_refl [in MapFacts]
MyMapFacts.fold_invariant2 [in MapFacts]
MyMapFacts.fold_left_assoc_map [in MapFacts]
MyMapFacts.fold_left_assoc [in MapFacts]
MyMapFacts.fold_left_assoc_map_find_nodup [in MapFacts]
MyMapFacts.fold_left_compat [in MapFacts]
MyMapFacts.fold_invariant [in MapFacts]
MyMapFacts.fold_invariant_cons [in MapFacts]
MyMapFacts.In_MapsTo [in MapFacts]
MyMapFacts.MapsTo_In [in MapFacts]
MyMapFacts.Mapsto_In [in MapFacts]
P
Path.cut_path [in Paths]Path.cut_path_aux [in Paths]
Path.decompose_app [in Paths]
Path.In_graph_edge_equiv [in Paths]
Path.in_path_in_graph [in Paths]
Path.minus_plus_plus_minus [in Paths]
Path.path_edge_charac [in Paths]
Path.path_end [in Paths]
Path.path_value_eq [in Paths]
Path.path_snd_ext [in Paths]
Path.path_trans [in Paths]
Path.path_eqlistA [in Paths]
Path.path_shorten_1 [in Paths]
Path.path_ends_in_graph [in Paths]
Path.path_nil_eq_end [in Paths]
Path.path_shorten_2 [in Paths]
Path.path_value_ge_edge [in Paths]
Path.pos_edge_pos_path [in Paths]
S
Shortest_path.remove_remove_cp [in Dijkstra]Shortest_path.path_init [in Dijkstra]
Shortest_path.null_init_3 [in Dijkstra]
Shortest_path.update_closed_inv [in Dijkstra]
Shortest_path.update_list_neq_aux [in Dijkstra]
Shortest_path.open_vertices_nb_eq [in Dijkstra]
Shortest_path.set_open_init [in Dijkstra]
Shortest_path.path_implies_reachable [in Dijkstra]
Shortest_path.list_as_OT.lt_not_eq [in Dijkstra]
Shortest_path.Dijkstra_optimal [in Dijkstra]
Shortest_path.init_finite [in Dijkstra]
Shortest_path.update_list_eq [in Dijkstra]
Shortest_path.Dijkstra_root [in Dijkstra]
Shortest_path.consistant_status [in Dijkstra]
Shortest_path.add_cp [in Dijkstra]
Shortest_path.nonoptimal_vertices_nb_eq_unreached [in Dijkstra]
Shortest_path.infinite_none_no_open [in Dijkstra]
Shortest_path.root_find_init [in Dijkstra]
Shortest_path.completeness_2 [in Dijkstra]
Shortest_path.set_open_iter [in Dijkstra]
Shortest_path.Dijkstra_graph [in Dijkstra]
Shortest_path.equivalence_eq_key [in Dijkstra]
Shortest_path.find_min_2 [in Dijkstra]
Shortest_path.add_remove_cp [in Dijkstra]
Shortest_path.path_construction [in Dijkstra]
Shortest_path.completeness [in Dijkstra]
Shortest_path.in_map_in_graph_init [in Dijkstra]
Shortest_path.list_as_OT.eq_trans [in Dijkstra]
Shortest_path.list_as_OT.lt_trans [in Dijkstra]
Shortest_path.list_as_OT.eq_dec [in Dijkstra]
Shortest_path.list_as_OT.eq_sym [in Dijkstra]
Shortest_path.correctness_aux [in Dijkstra]
Shortest_path.shortest_init [in Dijkstra]
Shortest_path.Dijkstra_graph_aux [in Dijkstra]
Shortest_path.first_iter_charac [in Dijkstra]
Shortest_path.Dijkstra_root_aux [in Dijkstra]
Shortest_path.nonoptimal_vertices_nb_eq_up [in Dijkstra]
Shortest_path.list_as_OT.eq_refl [in Dijkstra]
Shortest_path.shortest_iteration [in Dijkstra]
Shortest_path.iteration_pathmap_none [in Dijkstra]
Shortest_path.find_min_none_charac [in Dijkstra]
Shortest_path.iteration_root [in Dijkstra]
Shortest_path.dynamic_continuation [in Dijkstra]
Shortest_path.list_as_OT.compare [in Dijkstra]
Shortest_path.null_init_1 [in Dijkstra]
Shortest_path.root_find_iter [in Dijkstra]
Shortest_path.add_add_cp [in Dijkstra]
Shortest_path.path_iteration [in Dijkstra]
Shortest_path.iteration_graph [in Dijkstra]
Shortest_path.dynamic_init [in Dijkstra]
Shortest_path.null_init_2 [in Dijkstra]
Shortest_path.first_iter_not_opt [in Dijkstra]
Shortest_path.correctness [in Dijkstra]
Shortest_path.find_min_1 [in Dijkstra]
Shortest_path.iteration_finite [in Dijkstra]
Shortest_path.dynamic_iteration [in Dijkstra]
Shortest_path.update_list_neq [in Dijkstra]
Shortest_path.in_map_in_graph_iter [in Dijkstra]
Shortest_path.iteration_closed_charac [in Dijkstra]
Shortest_path.Dijkstra_path [in Dijkstra]
Shortest_path.first_iter_charac_2 [in Dijkstra]
Shortest_path.find_min_opt [in Dijkstra]
Shortest_path.update_list_eq_aux [in Dijkstra]
Shortest_path.remove_cp [in Dijkstra]
U
UDSpec.Add_edge_fail_vertex_u [in Unlabeled_spec]UDSpec.Add_edge_fail_edge_u [in Unlabeled_spec]
UDSpec.In_add_vertex_edge_u [in Unlabeled_spec]
UDSpec.In_add_vertex_u [in Unlabeled_spec]
UDSpec.In_remove_vertex_u [in Unlabeled_spec]
UDSpec.In_graph_remove_edge_vertex_u [in Unlabeled_spec]
UDSpec.In_graph_remove_edge_edge_pred_u [in Unlabeled_spec]
UDSpec.In_graph_add_edge_weak_vertex_u [in Unlabeled_spec]
UDSpec.In_graph_add_edge_weak_edge_u [in Unlabeled_spec]
UDSpec.In_graph_edge_add_edge_u [in Unlabeled_spec]
UDSpec.In_graph_remove_edge_edge_succ_u [in Unlabeled_spec]
UDSpec.In_remove_edge_u [in Unlabeled_spec]
UDSpec.In_graph_add_edge_edge_u [in Unlabeled_spec]
UDSpec.In_graph_add_edge_vertex_u [in Unlabeled_spec]
UDSpec.In_graph_edge_add_edge_2_u [in Unlabeled_spec]
Undirected_GraphMap.adj_remove_edge [in UndigraphMapImp]
Undirected_GraphMap.empty_graph_empty [in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge_in_ext [in UndigraphMapImp]
Undirected_GraphMap.mapsto_edge_equiv_pred [in UndigraphMapImp]
Undirected_GraphMap.In_graph_add_edge_edge [in UndigraphMapImp]
Undirected_GraphMap.mapsto_edge_equiv_succ [in UndigraphMapImp]
Undirected_GraphMap.adjacency_add_vertex [in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_diff [in UndigraphMapImp]
Undirected_GraphMap.adj_remove_edge_fst [in UndigraphMapImp]
Undirected_GraphMap.In_graph_remove_edge_edge_pred [in UndigraphMapImp]
Undirected_GraphMap.adjacency_remove_edge [in UndigraphMapImp]
Undirected_GraphMap.remove_neighbor_spec [in UndigraphMapImp]
Undirected_GraphMap.In_graph_remove_edge_edge_succ [in UndigraphMapImp]
Undirected_GraphMap.remove_map_adj_eq [in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge_add_edge [in UndigraphMapImp]
Undirected_GraphMap.In_ext_dec [in UndigraphMapImp]
Undirected_GraphMap.In_graph_add_edge_vertex [in UndigraphMapImp]
Undirected_GraphMap.Equal_remove_empty [in UndigraphMapImp]
Undirected_GraphMap.adjacency_remove_vertex [in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_spec [in UndigraphMapImp]
Undirected_GraphMap.In_graph_remove_edge_vertex [in UndigraphMapImp]
Undirected_GraphMap.In_graph_labeled_edge_spec [in UndigraphMapImp]
Undirected_GraphMap.In_graph_add_edge_weak_vertex [in UndigraphMapImp]
Undirected_GraphMap.adjacency_add_edge [in UndigraphMapImp]
Undirected_GraphMap.add_edge_adj [in UndigraphMapImp]
Undirected_GraphMap.In_remove_vertex [in UndigraphMapImp]
Undirected_GraphMap.edge_label_spec [in UndigraphMapImp]
Undirected_GraphMap.add_edge_adj_snd [in UndigraphMapImp]
Undirected_GraphMap.Mapsto_In [in UndigraphMapImp]
Undirected_GraphMap.add_edge_adj_fst [in UndigraphMapImp]
Undirected_GraphMap.EMapsto_In [in UndigraphMapImp]
Undirected_GraphMap.Add_edge_fail_edge [in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge_spec [in UndigraphMapImp]
Undirected_GraphMap.fold_succ_ne_spec [in UndigraphMapImp]
Undirected_GraphMap.adjacency_empty [in UndigraphMapImp]
Undirected_GraphMap.adj_remove_edge_notin [in UndigraphMapImp]
Undirected_GraphMap.Add_edge_fail_vertex [in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_eq [in UndigraphMapImp]
Undirected_GraphMap.remove_map_mapsto [in UndigraphMapImp]
Undirected_GraphMap.fold_edges_spec [in UndigraphMapImp]
Undirected_GraphMap.fold_vertices_spec [in UndigraphMapImp]
Undirected_GraphMap.adj_remove_edge_snd [in UndigraphMapImp]
Undirected_GraphMap.In_graph_labeled_vertex_spec [in UndigraphMapImp]
Undirected_GraphMap.In_graph_vertex_spec [in UndigraphMapImp]
Undirected_GraphMap.add_edge_adj_notin [in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_compat [in UndigraphMapImp]
Undirected_GraphMap.vertex_label_spec [in UndigraphMapImp]
Undirected_GraphMap.unw_adjacency [in UndigraphMapImp]
Undirected_GraphMap.In_add_vertex [in UndigraphMapImp]
Undirected_GraphMap.fold_pred_ne_spec [in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood_comm [in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge_add_edge_2 [in UndigraphMapImp]
Undirected_GraphMap.In_add_vertex_edge [in UndigraphMapImp]
Undirected_GraphMap.In_remove_edge [in UndigraphMapImp]
Undirected_GraphMap.link_edge_equiv [in UndigraphMapImp]
Undirected_GraphMap.In_graph_add_edge_weak_edge [in UndigraphMapImp]
Undirected_GraphMap.fold_succ_spec [in UndigraphMapImp]
Undirected_GraphMap.remove_map_adj [in UndigraphMapImp]
Undirected_GraphMap.fold_pred_spec [in UndigraphMapImp]
Undirected_GraphMap.permute_edge_in [in UndigraphMapImp]
Undirected_GraphMap.In_graph_add_edge_weak_edge_2 [in UndigraphMapImp]
UUSpec.Add_edge_fail_vertex_u [in Unlabeled_spec]
UUSpec.Add_edge_fail_edge_u [in Unlabeled_spec]
UUSpec.In_graph_remove_edge_vertex_u [in Unlabeled_spec]
UUSpec.In_graph_remove_edge_edge_pred_u [in Unlabeled_spec]
UUSpec.In_remove_edge_u [in Unlabeled_spec]
UUSpec.In_graph_add_edge_vertex_u [in Unlabeled_spec]
UUSpec.In_graph_add_edge_edge_u [in Unlabeled_spec]
UUSpec.In_graph_edge_add_edge_2_u [in Unlabeled_spec]
UUSpec.In_graph_remove_edge_edge_succ_u [in Unlabeled_spec]
UUSpec.In_add_vertex_edge_u [in Unlabeled_spec]
UUSpec.In_add_vertex_u [in Unlabeled_spec]
UUSpec.In_remove_vertex_u [in Unlabeled_spec]
UUSpec.In_graph_add_edge_weak_vertex_u [in Unlabeled_spec]
UUSpec.In_graph_edge_add_edge_u [in Unlabeled_spec]
UUSpec.In_graph_add_edge_weak_edge_u [in Unlabeled_spec]
Section Index
M
MyMapFacts.associative_fold_maps [in MapFacts]MyMapFacts.general_associative_fold [in MapFacts]
MyMapFacts.MapsTo_In [in MapFacts]
MyMapFacts.Submap [in MapFacts]
Notation Index
G
_ =G _ [in Graph_Properties]Constructor Index
D
Directed_GraphMap.Make_Graph [in DigraphMapImp]M
MyMapFacts.None_eq [in MapFacts]MyMapFacts.Some_eq [in MapFacts]
P
Path.path_post [in Paths]Path.path_self [in Paths]
S
Shortest_path.Reached [in Dijkstra]Shortest_path.Unreached [in Dijkstra]
Shortest_path.Open [in Dijkstra]
Shortest_path.list_as_OT.ltcons [in Dijkstra]
Shortest_path.Optimal [in Dijkstra]
Shortest_path.Make_pathmap [in Dijkstra]
Shortest_path.list_as_OT.lt_tail [in Dijkstra]
Shortest_path.list_as_OT.ltnil [in Dijkstra]
U
Undirected_GraphMap.Make_Graph [in UndigraphMapImp]Inductive Index
M
MyMapFacts.eq_map_option [in MapFacts]P
Path.path [in Paths]S
Shortest_path.status [in Dijkstra]Shortest_path.list_as_OT.lt_ [in Dijkstra]
Shortest_path.vertex_status [in Dijkstra]
Definition Index
C
Constructive_Undirected_Graph.In_ext [in Constructive_UndigraphInterface]Constructive_Directed_Graph.In_ext [in Constructive_DigraphInterface]
D
Directed_GraphMap.In_graph_labeled_edge [in DigraphMapImp]Directed_GraphMap.link [in DigraphMapImp]
Directed_GraphMap.fold_pred_ne [in DigraphMapImp]
Directed_Edge.fst_end [in Directed_edges]
Directed_Edge.incident [in Directed_edges]
Directed_GraphMap.empty_map [in DigraphMapImp]
Directed_GraphMap.In_graph_vertex [in DigraphMapImp]
Directed_GraphMap.add_vertex_map [in DigraphMapImp]
Directed_GraphMap.fold_vertices [in DigraphMapImp]
Directed_GraphMap.fold_pred [in DigraphMapImp]
Directed_GraphMap.adj_map [in DigraphMapImp]
Directed_GraphMap.fold_succ [in DigraphMapImp]
Directed_GraphMap.add_neighborhood [in DigraphMapImp]
Directed_Edge.snd_end [in Directed_edges]
Directed_GraphMap.remove_edge_map [in DigraphMapImp]
Directed_GraphMap.empty_graph [in DigraphMapImp]
Directed_GraphMap.pred [in DigraphMapImp]
Directed_GraphMap.is_pred [in DigraphMapImp]
Directed_GraphMap.add_edge_map [in DigraphMapImp]
Directed_GraphMap.fold_edges [in DigraphMapImp]
Directed_GraphMap.is_succ [in DigraphMapImp]
Directed_GraphMap.succ [in DigraphMapImp]
Directed_GraphMap.V [in DigraphMapImp]
Directed_Edge.permute [in Directed_edges]
Directed_GraphMap.predecessors [in DigraphMapImp]
Directed_GraphMap.remove_vertex [in DigraphMapImp]
Directed_GraphMap.E [in DigraphMapImp]
Directed_GraphMap.successors [in DigraphMapImp]
Directed_GraphMap.is_labeled_pred [in DigraphMapImp]
Directed_GraphMap.add_edge_w [in DigraphMapImp]
Directed_GraphMap.In_graph_labeled_vertex [in DigraphMapImp]
Directed_GraphMap.maptype [in DigraphMapImp]
Directed_GraphMap.fold_succ_ne [in DigraphMapImp]
Directed_GraphMap.is_labeled_succ [in DigraphMapImp]
Directed_GraphMap.edge_label [in DigraphMapImp]
Directed_GraphMap.remove_edge [in DigraphMapImp]
Directed_GraphMap.t [in DigraphMapImp]
Directed_GraphMap.remove_neighbor [in DigraphMapImp]
Directed_GraphMap.add_edge [in DigraphMapImp]
Directed_GraphMap.In_graph_edge [in DigraphMapImp]
Directed_GraphMap.remove_map [in DigraphMapImp]
Directed_GraphMap.add_vertex [in DigraphMapImp]
Directed_GraphMap.vertex_label [in DigraphMapImp]
Directed_GraphMap.In_ext [in DigraphMapImp]
G
GraphProps.eq [in Graph_Properties]M
MyMapFacts.EqualMap [in MapFacts]MyMapFacts.SubMap [in MapFacts]
N
Nat_Labels.NodeLabel [in Labels]Nat_Labels.EdgeLabel [in Labels]
P
Path.eval [in Paths]S
Shortest_path.nonoptimal_vertices_nb [in Dijkstra]Shortest_path.init [in Dijkstra]
Shortest_path.null_init [in Dijkstra]
Shortest_path.update [in Dijkstra]
Shortest_path.Dijkstra_measure [in Dijkstra]
Shortest_path.iteration_pathmap [in Dijkstra]
Shortest_path.Dijkstra [in Dijkstra]
Shortest_path.list_as_OT.eq [in Dijkstra]
Shortest_path.first_iter [in Dijkstra]
Shortest_path.shortest_path_length [in Dijkstra]
Shortest_path.iteration [in Dijkstra]
Shortest_path.shortest_path [in Dijkstra]
Shortest_path.equiv_edge_eq [in Dijkstra]
Shortest_path.list_as_OT.lt [in Dijkstra]
Shortest_path.dynamic_prog [in Dijkstra]
Shortest_path.update_list [in Dijkstra]
Shortest_path.correct_path [in Dijkstra]
Shortest_path.list_as_OT.t [in Dijkstra]
Shortest_path.init_dijkstra [in Dijkstra]
Shortest_path.find_min [in Dijkstra]
U
Undirected_GraphMap.adj [in UndigraphMapImp]Undirected_GraphMap.fold_vertices [in UndigraphMapImp]
Undirected_GraphMap.predecessors [in UndigraphMapImp]
Undirected_GraphMap.remove_vertex [in UndigraphMapImp]
Undirected_GraphMap.remove_map [in UndigraphMapImp]
Undirected_GraphMap.pred [in UndigraphMapImp]
Undirected_GraphMap.maptype [in UndigraphMapImp]
Undirected_GraphMap.add_neighborhood [in UndigraphMapImp]
Undirected_GraphMap.In_graph_vertex [in UndigraphMapImp]
Undirected_GraphMap.In_ext [in UndigraphMapImp]
Undirected_GraphMap.adjacent [in UndigraphMapImp]
Undirected_GraphMap.successors [in UndigraphMapImp]
Undirected_GraphMap.remove_neighbor [in UndigraphMapImp]
Undirected_GraphMap.V [in UndigraphMapImp]
Undirected_GraphMap.fold_pred [in UndigraphMapImp]
Undirected_GraphMap.edge_label [in UndigraphMapImp]
Undirected_GraphMap.add_edge [in UndigraphMapImp]
Undirected_GraphMap.link [in UndigraphMapImp]
Undirected_GraphMap.is_labeled_adj [in UndigraphMapImp]
Undirected_GraphMap.fold_succ_ne [in UndigraphMapImp]
Undirected_GraphMap.In_graph_edge [in UndigraphMapImp]
Undirected_GraphMap.add_edge_w [in UndigraphMapImp]
Undirected_GraphMap.t [in UndigraphMapImp]
Undirected_GraphMap.fold_pred_ne [in UndigraphMapImp]
Undirected_GraphMap.add_vertex [in UndigraphMapImp]
Undirected_GraphMap.fold_succ [in UndigraphMapImp]
Undirected_GraphMap.remove_edge_map [in UndigraphMapImp]
Undirected_GraphMap.empty_map [in UndigraphMapImp]
Undirected_GraphMap.vertex_label [in UndigraphMapImp]
Undirected_GraphMap.add_vertex_map [in UndigraphMapImp]
Undirected_GraphMap.succ [in UndigraphMapImp]
Undirected_GraphMap.empty_graph [in UndigraphMapImp]
Undirected_GraphMap.E [in UndigraphMapImp]
Undirected_GraphMap.adj_map [in UndigraphMapImp]
Undirected_GraphMap.remove_edge [in UndigraphMapImp]
Undirected_GraphMap.In_graph_labeled_edge [in UndigraphMapImp]
Undirected_GraphMap.fold_edges [in UndigraphMapImp]
Undirected_GraphMap.In_graph_labeled_vertex [in UndigraphMapImp]
Undirected_GraphMap.is_adj [in UndigraphMapImp]
Undirected_GraphMap.add_edge_map [in UndigraphMapImp]
Axiom Index
C
Constructive_Undirected_Graph.In_graph_labeled_edge_spec [in Constructive_UndigraphInterface]Constructive_Directed_Graph.add_edge [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_edge_in_ext [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_vertex [in Constructive_DigraphInterface]
Constructive_Directed_Graph.edge_label_spec [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.mapsto_edge_equiv_pred [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_remove_edge_edge_succ [in Constructive_DigraphInterface]
Constructive_Directed_Graph.Add_edge_fail_edge [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.t [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_edge [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_edge_spec [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_labeled_vertex [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.link [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_succ_spec [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_edge_add_edge_2 [in Constructive_DigraphInterface]
Constructive_Directed_Graph.vertex_label_spec [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_edge [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.remove_edge [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.V [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.Add_edge_fail_vertex [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_pred_ne [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.mapsto_edge_equiv_pred [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_labeled_edge [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_add_edge_edge [in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_edge_spec [in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_labeled_vertex [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_add_edge_weak_edge [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.permute_edge_in [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_edges [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_succ_ne [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_remove_edge_vertex [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_pred_spec [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.remove_vertex [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_add_edge_weak_edge [in Constructive_DigraphInterface]
Constructive_Directed_Graph.successors [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_succ [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_edge_add_edge [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.vertex_label [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_pred [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_vertex_spec [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.empty_graph [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_succ_ne [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_remove_edge [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.E [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_pred_ne [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_edge_add_edge_2 [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_labeled_vertex_spec [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.vertex_label [in Constructive_DigraphInterface]
Constructive_Directed_Graph.remove_edge [in Constructive_DigraphInterface]
Constructive_Directed_Graph.mapsto_edge_equiv_succ [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_vertex [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_succ_ne_spec [in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_edges [in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_labeled_edge_spec [in Constructive_DigraphInterface]
Constructive_Directed_Graph.add_vertex [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_vertices_spec [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.link_edge_equiv [in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_succ [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.add_edge_w [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_pred_ne_spec [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_edge_in_ext [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_remove_vertex [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_vertex_spec [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.successors [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_remove_edge_edge_pred [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.vertex_label_spec [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_add_vertex [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.Add_edge_fail_edge [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.link_edge_equiv [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.V [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_remove_edge_edge_succ [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_vertices [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.mapsto_edge_equiv_succ [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_add_edge_vertex [in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_graph_add_edge_weak_vertex [in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_add_vertex_edge [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.edge_label [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_add_edge_edge [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_edge_add_edge [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_remove_edge_vertex [in Constructive_DigraphInterface]
Constructive_Directed_Graph.edge_label [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_add_vertex_edge [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.E [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.add_vertex [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_add_edge_vertex [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.In_graph_remove_edge_edge_pred [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_vertices_spec [in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_add_vertex [in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_pred_ne_spec [in Constructive_DigraphInterface]
Constructive_Directed_Graph.remove_vertex [in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_edges_spec [in Constructive_DigraphInterface]
Constructive_Directed_Graph.empty_graph [in Constructive_DigraphInterface]
Constructive_Directed_Graph.Add_edge_fail_vertex [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.add_edge [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.fold_succ_spec [in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_pred [in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_remove_vertex [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.fold_edges_spec [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.add_edge_w [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.edge_label_spec [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.t [in Constructive_DigraphInterface]
Constructive_Directed_Graph.In_remove_edge [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.In_graph_add_edge_weak_vertex [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.link [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_pred_spec [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.fold_succ_ne_spec [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_labeled_vertex_spec [in Constructive_DigraphInterface]
Constructive_Directed_Graph.predecessors [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.predecessors [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.In_graph_labeled_edge [in Constructive_DigraphInterface]
Constructive_Directed_Graph.fold_vertices [in Constructive_DigraphInterface]
D
Directed_Graph.V [in DigraphInterface]Directed_Graph.link [in DigraphInterface]
Directed_Graph.fold_pred [in DigraphInterface]
Directed_Graph.fold_succ [in DigraphInterface]
Directed_Graph.In_graph_labeled_vertex_spec [in DigraphInterface]
Directed_Graph.fold_succ_ne [in DigraphInterface]
Directed_Graph.In_graph_labeled_edge [in DigraphInterface]
Directed_Graph.E [in DigraphInterface]
Directed_Graph.In_graph_edge_spec [in DigraphInterface]
Directed_Graph.fold_vertices [in DigraphInterface]
Directed_Graph.fold_pred_ne [in DigraphInterface]
Directed_Graph.vertex_label_spec [in DigraphInterface]
Directed_Graph.mapsto_edge_equiv_pred [in DigraphInterface]
Directed_Graph.In_graph_labeled_edge_spec [in DigraphInterface]
Directed_Graph.edge_label_spec [in DigraphInterface]
Directed_Graph.edge_label [in DigraphInterface]
Directed_Graph.In_graph_vertex [in DigraphInterface]
Directed_Graph.In_graph_labeled_vertex [in DigraphInterface]
Directed_Graph.In_graph_edge_in_ext [in DigraphInterface]
Directed_Graph.fold_succ_spec [in DigraphInterface]
Directed_Graph.link_edge_equiv [in DigraphInterface]
Directed_Graph.fold_edges [in DigraphInterface]
Directed_Graph.fold_succ_ne_spec [in DigraphInterface]
Directed_Graph.fold_edges_spec [in DigraphInterface]
Directed_Graph.In_graph_edge [in DigraphInterface]
Directed_Graph.mapsto_edge_equiv_succ [in DigraphInterface]
Directed_Graph.fold_pred_spec [in DigraphInterface]
Directed_Graph.predecessors [in DigraphInterface]
Directed_Graph.In_graph_vertex_spec [in DigraphInterface]
Directed_Graph.fold_vertices_spec [in DigraphInterface]
Directed_Graph.t [in DigraphInterface]
Directed_Graph.vertex_label [in DigraphInterface]
Directed_Graph.fold_pred_ne_spec [in DigraphInterface]
Directed_Graph.successors [in DigraphInterface]
L
Labels.EdgeLabel [in Labels]Labels.NodeLabel [in Labels]
U
Undirected_Graph.In_graph_edge_spec [in UndigraphInterface]Undirected_Graph.fold_edges_spec [in UndigraphInterface]
Undirected_Graph.fold_succ_spec [in UndigraphInterface]
Undirected_Graph.fold_pred_ne_spec [in UndigraphInterface]
Undirected_Graph.In_graph_labeled_vertex [in UndigraphInterface]
Undirected_Graph.fold_edges [in UndigraphInterface]
Undirected_Graph.t [in UndigraphInterface]
Undirected_Graph.E [in UndigraphInterface]
Undirected_Graph.edge_label [in UndigraphInterface]
Undirected_Graph.permute_edge_in [in UndigraphInterface]
Undirected_Graph.fold_vertices_spec [in UndigraphInterface]
Undirected_Graph.mapsto_edge_equiv_succ [in UndigraphInterface]
Undirected_Graph.mapsto_edge_equiv_pred [in UndigraphInterface]
Undirected_Graph.fold_succ_ne [in UndigraphInterface]
Undirected_Graph.In_graph_vertex_spec [in UndigraphInterface]
Undirected_Graph.In_graph_edge_in_ext [in UndigraphInterface]
Undirected_Graph.V [in UndigraphInterface]
Undirected_Graph.fold_vertices [in UndigraphInterface]
Undirected_Graph.In_graph_labeled_edge_spec [in UndigraphInterface]
Undirected_Graph.fold_pred [in UndigraphInterface]
Undirected_Graph.link_edge_equiv [in UndigraphInterface]
Undirected_Graph.In_graph_labeled_edge [in UndigraphInterface]
Undirected_Graph.predecessors [in UndigraphInterface]
Undirected_Graph.vertex_label [in UndigraphInterface]
Undirected_Graph.fold_pred_ne [in UndigraphInterface]
Undirected_Graph.vertex_label_spec [in UndigraphInterface]
Undirected_Graph.In_graph_edge [in UndigraphInterface]
Undirected_Graph.link [in UndigraphInterface]
Undirected_Graph.fold_succ_ne_spec [in UndigraphInterface]
Undirected_Graph.fold_succ [in UndigraphInterface]
Undirected_Graph.fold_pred_spec [in UndigraphInterface]
Undirected_Graph.successors [in UndigraphInterface]
Undirected_Graph.edge_label_spec [in UndigraphInterface]
Undirected_Graph.In_graph_vertex [in UndigraphInterface]
Undirected_Graph.In_graph_labeled_vertex_spec [in UndigraphInterface]
Module Index
C
Constructive_Undirected_Graph.VertexMap [in Constructive_UndigraphInterface]Constructive_Directed_Graph.Edge [in Constructive_DigraphInterface]
Constructive_Directed_Graph.EdgeMap [in Constructive_DigraphInterface]
Constructive_Directed_Graph.EMapFacts [in Constructive_DigraphInterface]
Constructive_Directed_Graph [in Constructive_DigraphInterface]
Constructive_Directed_Graph.VertexMap [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.EdgeMap [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.Edge [in Constructive_UndigraphInterface]
Constructive_Undirected_Graph.VMapFacts [in Constructive_UndigraphInterface]
Constructive_Directed_Graph.VMapFacts [in Constructive_DigraphInterface]
Constructive_Undirected_Graph.EMapFacts [in Constructive_UndigraphInterface]
D
D [in Benchmark]Directed_Graph.EMapFacts [in DigraphInterface]
Directed_Edge.OTPairFacts [in Directed_edges]
Directed_GraphMap.EMapFacts [in DigraphMapImp]
Directed_Edge.VertexPair [in Directed_edges]
Directed_GraphMap.Edge [in DigraphMapImp]
Directed_GraphMap [in DigraphMapImp]
Directed_Graph.EdgeMap [in DigraphInterface]
Directed_GraphMap.VertexMap [in DigraphMapImp]
Directed_Edge.OTFacts [in Directed_edges]
Directed_Graph.VertexMap [in DigraphInterface]
Directed_Graph.VMapFacts [in DigraphInterface]
Directed_Edge [in Directed_edges]
Directed_GraphMap.VMapFacts [in DigraphMapImp]
Directed_GraphMap.EdgeMap [in DigraphMapImp]
Directed_Graph [in DigraphInterface]
Directed_Graph.Edge [in DigraphInterface]
E
Eadd [in Common]eqlistAFacts [in Common]
G
G [in Benchmark]GraphProps [in Graph_Properties]
L
Labels [in Labels]M
MyMapFacts [in MapFacts]MyMapFacts.MapFacts [in MapFacts]
N
Nat_Labels [in Labels]P
Path [in Paths]Path.P [in Paths]
S
Shortest_path.EdgeList [in Dijkstra]Shortest_path.CoupleSet [in Dijkstra]
Shortest_path.EA [in Dijkstra]
Shortest_path.Couple [in Dijkstra]
Shortest_path.PS [in Dijkstra]
Shortest_path.Couple_ [in Dijkstra]
Shortest_path.eqlistAF [in Dijkstra]
Shortest_path.list_as_OT [in Dijkstra]
Shortest_path.list_as_OT.OP [in Dijkstra]
Shortest_path [in Dijkstra]
Shortest_path.P [in Dijkstra]
Shortest_path.PPS [in Dijkstra]
U
UDSpec [in Unlabeled_spec]UDSpec.Props [in Unlabeled_spec]
Undirected_Graph [in UndigraphInterface]
Undirected_GraphMap.Edge [in UndigraphMapImp]
Undirected_Graph.EdgeMap [in UndigraphInterface]
Undirected_Graph.VMapFacts [in UndigraphInterface]
Undirected_GraphMap.EdgeMap [in UndigraphMapImp]
Undirected_GraphMap.VMapFacts [in UndigraphMapImp]
Undirected_Graph.EMapFacts [in UndigraphInterface]
Undirected_Graph.Edge [in UndigraphInterface]
Undirected_GraphMap.EMapFacts [in UndigraphMapImp]
Undirected_GraphMap [in UndigraphMapImp]
Undirected_Graph.VertexMap [in UndigraphInterface]
Undirected_GraphMap.VertexMap [in UndigraphMapImp]
UUSpec [in Unlabeled_spec]
UUSpec.Props [in Unlabeled_spec]
Variable Index
M
MyMapFacts.associative_fold_maps.eqA_refl [in MapFacts]MyMapFacts.associative_fold_maps.eqA_trans [in MapFacts]
MyMapFacts.associative_fold_maps.B [in MapFacts]
MyMapFacts.associative_fold_maps.eqA [in MapFacts]
MyMapFacts.associative_fold_maps.A [in MapFacts]
MyMapFacts.general_associative_fold.B [in MapFacts]
MyMapFacts.general_associative_fold.eqA_refl [in MapFacts]
MyMapFacts.general_associative_fold.eqA [in MapFacts]
MyMapFacts.general_associative_fold.eqA_trans [in MapFacts]
MyMapFacts.general_associative_fold.A [in MapFacts]
MyMapFacts.general_associative_fold.eqB [in MapFacts]
MyMapFacts.MapsTo_In.A [in MapFacts]
MyMapFacts.Submap.A [in MapFacts]
Library Index
B
BenchmarkC
CommonConstructive_DigraphInterface
Constructive_UndigraphInterface
D
DigraphInterfaceDigraphMapImp
Dijkstra
Directed_edges
E
ExtractionG
Graph_PropertiesL
LabelsM
MapFactsP
PathsU
UndigraphInterfaceUndigraphMapImp
Unlabeled_spec
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (706 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (275 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (112 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (67 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
This page has been generated by coqdoc