Mercurial > hg > Members > atton > delta_monad
diff agda/similar.agda @ 28:6e6d646d7722
Split basic functions to file
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 07 Oct 2014 14:55:40 +0900 |
parents | 742e62fc63e4 |
children | e0ba1bf564dd |
line wrap: on
line diff
--- a/agda/similar.agda Tue Oct 07 14:53:56 2014 +0900 +++ b/agda/similar.agda Tue Oct 07 14:55:40 2014 +0900 @@ -1,23 +1,16 @@ open import list +open import basic open import Relation.Binary.PropositionalEquality open ≡-Reasoning module similar where -id : {A : Set} -> A -> A -id x = x - -postulate String : Set -postulate show : {A : Set} -> A -> String - data Similar (A : Set) : Set where similar : List String -> A -> List String -> A -> Similar A - fmap : {A B : Set} -> (A -> B) -> (Similar A) -> (Similar B) fmap f (similar xs x ys y) = similar xs (f x) ys (f y) - mu : {A : Set} -> Similar (Similar A) -> Similar A mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y @@ -31,9 +24,6 @@ returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y -_∙_ : {A B C : Set} -> (A -> B) -> (B -> C) -> (A -> C) -f ∙ g = \x -> g (f x) - monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu monad-law-1 = {!!}