Mercurial > hg > Members > kono > Proof > category
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 :: [] }