# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1571189743 -32400
# Node ID ff4f57e17df57353f1b8cb90ad603d65bff995ae
# Parent  f443cd9de556f2cd412bbee889b5050c1e57adb2
...

diff -r f443cd9de556 -r ff4f57e17df5 agda/chap0.agda
--- a/agda/chap0.agda	Tue Oct 15 16:05:34 2019 +0900
+++ b/agda/chap0.agda	Wed Oct 16 10:35:43 2019 +0900
@@ -71,8 +71,8 @@
     e012a-4 : edge012a 4 5
     e012a-5 : edge012a 5 1
 
-graph012a : Graph {Zero} {Zero}
-graph012a = record { vertex = ℕ  ; edge = edge012a }
+graph012a : Graph {Zero} {Zero} 
+graph012a = record { vertex = ℕ  ; edge = edge012a } -- ; e-list =  e012a-1 ∷ e012a-2 ∷ e012a-3 ∷ e012a-4 ∷ e012a-5 ∷ [] }
 
 data edge012b :  ℕ → ℕ →  Set where
     e012b-1 : edge012b 1 2
@@ -103,3 +103,6 @@
 dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
 
 
+all-edge-012a : List ?
+all-edge-012a = e012a-1 ∷ e012a-2 ∷ e012a-3 ∷ e012a-4 ∷ e012a-5 ∷ []
+