From 9f73b5d809576638cba602d3fed819bd1de46333 Mon Sep 17 00:00:00 2001 From: Andrey Mokhov Date: Sun, 16 Apr 2017 04:25:28 +0100 Subject: [PATCH] Minor fixes --- src/Graph.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Graph.agda b/src/Graph.agda index 8104d8e..0e28667 100644 --- a/src/Graph.agda +++ b/src/Graph.agda @@ -1,9 +1,9 @@ -module Graph (V : Set) where +module Graph (A : Set) where -- Core graph construction primitives data Graph : Set where ε : Graph -- Empty graph - [_] : V -> Graph -- Graph comprising a single vertex + [_] : A -> Graph -- Graph comprising a single vertex _+_ : Graph -> Graph -> Graph -- Overlay two graphs _*_ : Graph -> Graph -> Graph -- Connect two graphs @@ -57,4 +57,3 @@ L {connect} {x} {y} {z} eq = *left-congruence {x} {y} {z} eq R : ∀ {op : BinaryOperator} -> ∀ {x y z} -> x ≡ y -> apply op z x ≡ apply op z y R {overlay} {x} {y} {z} eq = +right-congruence {x} {y} {z} eq R {connect} {x} {y} {z} eq = *right-congruence {x} {y} {z} eq -