changeset 165:a4200348a33d

fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Aug 2013 15:44:37 +0900
parents ab186f0e7b7a
children 2246a7d67ba3
files free-monoid.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Mon Aug 19 14:02:41 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 15:44:37 2013 +0900
@@ -255,7 +255,7 @@
                              ≡⟨ sym ( mdistr g ) ⟩
                                 (morph g) ( x :: xs )
                              ∎   where
-                          lemma-ext3 :  ∀{ x : a } -> (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )
-                          lemma-ext3 {x} = lemma-ext2 { x :: [] }
+                         lemma-ext3 :  ∀{ x : a } -> (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )
+                         lemma-ext3 {x} = lemma-ext2 { x :: [] }