changeset | 575de2e38385 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Fix names left/right unity law |
files |
changeset | d205ff1e406f |
---|---|
branch | |
bookmark | |
tag | InfiniteDeltaWithMonad |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Cleanup proofs |
files |
changeset | ac45d065cbf2 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove all Monad-laws for Delta with Monad |
files |
changeset | d57c88171f38 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove assciation-law for DeltaM on (S O) |
files |
changeset | d9a30f696933 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Fix association-law for DeltaM in (S n) |
files |
changeset | d56596e4e784 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove left-unity-law for DeltaM |
files |
changeset | 5902b2a24abf |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove mu-is-nt for DeltaM with fmap-equiv |
files |
changeset | 6dcc68ef8f96 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove right-unity-law for DeltaM |
files |
changeset | 48b44bd85056 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Fix proof natural transformation for deltaM-eta |
files |
changeset | 53cb21845dea |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove association-law for DeltaM |
files |
changeset | 6f86b55bf8b4 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Temporary commit : Proving association-law .... |
files |
changeset | f02c5ad4a327 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove association-law for DeltaM by (S O) pattern with definition changes |
files |
changeset | e6bcc7467335 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Temporary commit : Proving association-law ... |
files |
changeset | 08403eb8db8b |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove natural transformation for deltaM-eta |
files |
changeset | 0a3b6cb91a05 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove left-unity-law for DeltaM |
files |
changeset | 9fe3d0bd1149 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Prove right-unity-law on DeltaM |
files |
changeset | ebd0d6e2772c |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Trying redenition Delta with length constraints |
files |
changeset | a271f3ff1922 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Delte type dependencie in Monad record for escape implicit type conflict |
files |
changeset | 9c62373bd474 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Trying right-unity-law on DeltaM. but do not fit implicit type in eta... |
files |
changeset | b7f0879e854e |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Trying Monad-laws for DeltaM |
files |