Graph.idr

module Data.Graph

import Data.Vect

data Edge e = MkEdge e e

data Graph : Nat −> Nat −> Type −> Type −> Type where
  MkGraph : Vect m v −> Vect n (Edge k) −> Graph m n v k