1 (* summary of hypermap.ml file *)
5 (* `orbit_map f x` set of iterates of x under f. *)
6 exist_hypermap;; (* existence theorem for hypermap type *)
7 hypermap_tybij;; (* type construction of hypermap *)
8 dart;; (* extracts darts *)
9 edge_map;; (* extracts edge_map *)
10 node_map;; (* extracts node_map *)
11 face_map;; (* extracts face_map *)
13 edge;; (* orbit under edge map *)
14 node;; (* orbit under node map *)
15 face ;; (* orbit under face map *)
17 (* paths done by a new recursive definition *)
18 comb_component;; (* combinatorial component *)
19 set_of_orbits;; (* of a permutation f *)
20 number_of_orbits;; (* cardinality *)
22 edge_set;; (* set of all edges *)
25 set_of_components;; (* set of all combinatorial components *)
30 number_of_components;;
41 edge_path;; (* `edge_path H x i = e^i x` *)
45 (* contour path stuff.... *)
47 shift;; (* rotates e,n,f by triality *)
49 (* walkup transformations *)
52 iso;; (* isomorphism of hypermap *)