Mercurial > hg > Members > kono > Proof > automaton

changeset 54:ff4f57e17df5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 16 Oct 2019 10:35:43 +0900
parents f443cd9de556
children ba5ee7eb2866
files agda/chap0.agda
diffstat 1 files changed, 5 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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 ∷ []
+