on bf4e535 help sign in
8 lines 186 B history raw
1module Data.Graph
3import Data.Vect
5data Edge e = MkEdge e e
7data Graph : Nat −> Nat −> Type −> Type −> Type where
8 MkGraph : Vect m v −> Vect n (Edge k) −> Graph m n v k