erwig.idr

module Graph

%default total
%access public

Node : Type
Node = Nat

Adj : Type -> Type
Adj a = List (a, Node)

Context : Type -> Type -> Type
Context a b = (Adj b, Node, a, Adj b)

data Graph : Type -> Type -> Type
data Graph a b = Empty | (&) (Context a b) (Graph a b)

node : Node
node = Z

adj : Adj String
adj = [("one", Z)]

adj2 : Adj String
adj2 = [("two", (S Z))]

context : Context String String
context = (adj, node, "a", adj2)

g : Graph String String
g = (&) context Empty