Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
Require Import Basics.Overture.Require Import Basics.Overture.
(** * Graphs *)
(** A [Graph] is a type [graph0] of points together with a type [graph1] of arrows between each points. *)
Record Graph := {
graph0 : Type;
graph1 : graph0 -> graph0 -> Type;
}.
Coercion graph0 : Graph >-> Sortclass.
Coercion graph1 : Graph >-> Funclass.