Minor revision

.travis.yml

@@ -9,7 +9,7 @@ before_install:
 - docker pull scottfleischman/agda:2.5.2
 
 env:
-- AGDA_FILE="src/API/Laws.agda"
+- AGDA_FILE="src/API/Theorems.agda"
 
 script:
 - docker run -v $TRAVIS_BUILD_DIR:/opt/agda-build scottfleischman/agda:2.5.2 /bin/sh -c 'cd /opt/agda-build; agda '$AGDA_FILE

src/API.agda

@@ -1,6 +1,6 @@
 module API where
 
-open import Graph
+open import Algebra
 open import Prelude
 
 empty : ∀ {A} -> Graph A

src/API/Laws.agda → src/API/Theorems.agda

@@ -1,10 +1,10 @@
-module API.Laws where
+module API.Theorems where
 
+open import Algebra
+open import Algebra.Theorems
 open import API
-open import Graph
 open import Prelude
 open import Reasoning
-open import Theorems
 
 -- vertices [x] == vertex x
 vertices-vertex : ∀ {A} {x : A} -> vertices (x :: []) ≡ vertex x
@@ -18,4 +18,4 @@ vertices-clique {a} {_ :: t} = ⊆transitivity (⊆right-monotony (vertices-cliq
 -- clique (xs ++ ys) == connect (clique xs) (clique ys)
 connect-clique : ∀ {A} {xs ys : List A} -> clique (xs ++ ys) ≡ connect (clique xs) (clique ys)
 connect-clique {_} {[]}     = symmetry *left-identity
-connect-clique {a} {h :: t} = R (connect-clique {a} {t}) >> *associativity
+connect-clique {a} {_ :: t} = R (connect-clique {a} {t}) >> *associativity

src/Graph.agda → src/Algebra.agda

@@ -1,4 +1,4 @@
-module Graph where
+module Algebra where
 
 -- Core graph construction primitives
 data Graph (A : Set) : Set where

src/Theorems.agda → src/Algebra/Theorems.agda

@@ -1,6 +1,6 @@
-module Theorems where
+module Algebra.Theorems where
 
-open import Graph
+open import Algebra
 open import Reasoning
 
 +pre-idempotence : ∀ {A} {x : Graph A} -> x + x + ε ≡ x

src/Prelude.agda

@@ -18,14 +18,14 @@ data List (A : Set) : Set where
 
 infixr 20 _::_
 
+_++_ : ∀ {A} -> List A -> List A -> List A
+[] ++ l = l
+(x :: xs) ++ l = x :: (xs ++ l)
+
 foldr : ∀ {A B : Set} -> (A -> B -> B) -> B -> List A -> B
 foldr f b [] = b
 foldr f b (x :: xs) = f x (foldr f b xs)
 
 map : ∀ {A B} -> (A -> B) -> List A -> List B
 map f [] = []
 map f (x :: xs) = f x :: map f xs
-
-_++_ : ∀ {A} -> List A -> List A -> List A
-[] ++ l = l
-(x :: xs) ++ l = x :: (xs ++ l)

src/Reasoning.agda

@@ -1,6 +1,6 @@
 module Reasoning where
 
-open import Graph
+open import Algebra
 
 -- Standard syntax sugar for writing equational proofs
 infix 4 _≈_