2015-03-24 |
Yasutaka Higa |
Add an example used multi types on Delta
default tip
|
2015-02-27 |
Yasutaka Higa |
Add prototype Delta for modification with type changes
|
2015-02-25 |
Yasutaka Higa |
Fix names left/right unity law
|
2015-02-25 |
Yasutaka Higa |
Merge
|
2015-02-25 |
Yasutaka Higa |
Add sort example using Delta/DeltaM
|
2015-02-15 |
Yasutaka Higa |
case-sensitive collision resolve : Rename delta.hs -> Delta.hs
|
2015-02-15 |
Yasutaka Higa |
Merge some commits
|
2015-02-15 |
Yasutaka Higa |
Fix delta/Delta filename collision in hg
|
2015-02-15 |
Yasutaka Higa |
Rename function in example
|
2015-02-15 |
Yasutaka Higa |
Adjust codes
|
2015-02-15 |
Yasutaka Higa |
Delete unnecessary lines
|
2015-02-07 |
Yasutaka Higa |
Update Example
|
2015-02-06 |
Yasutaka Higa |
Rename and split with module for haskell codes
|
2015-02-06 |
Yasutaka Higa |
Create directory for haskell codes
|
2015-02-03 |
Yasutaka Higa |
Added tag InfiniteDeltaWithMonad for changeset d205ff1e406f
|
2015-02-03 |
Yasutaka Higa |
Cleanup proofs
InfiniteDeltaWithMonad
|
2015-02-03 |
Yasutaka Higa |
Prove all Monad-laws for Delta with Monad
|
2015-02-03 |
Yasutaka Higa |
Prove assciation-law for DeltaM on (S O)
|
2015-02-03 |
Yasutaka Higa |
Fix association-law for DeltaM in (S n)
|
2015-02-03 |
Yasutaka Higa |
Prove left-unity-law for DeltaM
|
2015-02-03 |
Yasutaka Higa |
Prove mu-is-nt for DeltaM with fmap-equiv
|
2015-02-02 |
Yasutaka Higa |
Prove right-unity-law for DeltaM
|
2015-02-02 |
Yasutaka Higa |
Fix proof natural transformation for deltaM-eta
|
2015-02-02 |
Yasutaka Higa |
Fix proof functor for DeltaM
|
2015-02-02 |
Yasutaka Higa |
Fix Monad-proof for Delta
|
2015-02-02 |
Yasutaka Higa |
Refactor monad definition
|
2015-02-02 |
Yasutaka Higa |
Refactor DeltaM definition
|
2015-02-02 |
Yasutaka Higa |
ReDefine DeltaM-mu in Haskell
|
2015-02-02 |
Yasutaka Higa |
Prove association-law for DeltaM
|
2015-02-02 |
Yasutaka Higa |
Temporary commit : Proving association-law ....
|
2015-02-01 |
Yasutaka Higa |
Prove association-law for DeltaM by (S O) pattern with definition changes
|
2015-02-01 |
Yasutaka Higa |
Temporary commit : Proving association-law ...
|
2015-01-30 |
Yasutaka Higa |
Prove natural transformation for deltaM-eta
|
2015-01-30 |
Yasutaka Higa |
Delte trying code
|
2015-01-30 |
Yasutaka Higa |
Prove left-unity-law for DeltaM
|
2015-01-29 |
Yasutaka Higa |
Prove right-unity-law on DeltaM
|
2015-01-28 |
Yasutaka Higa |
Rewrite Functor-laws for DeltaM
|
2015-01-28 |
Yasutaka Higa |
Redefine DeltaM that length fixed
|
2015-01-28 |
Yasutaka Higa |
Delete comment outed temporary code
|
2015-01-28 |
Yasutaka Higa |
Prove monad-laws for length fixed infinite Delta
|
2015-01-27 |
Yasutaka Higa |
Delete Revision
|
2015-01-27 |
Yasutaka Higa |
Retrying prove monad-laws for delta
|
2015-01-26 |
Yasutaka Higa |
Trying redenition Delta with length constraints
|
2015-01-26 |
Yasutaka Higa |
Delte type dependencie in Monad record for escape implicit type conflict
|
2015-01-25 |
Yasutaka Higa |
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
|
2015-01-25 |
Yasutaka Higa |
Fix bind definition on DeltaM. use mu.
|
2015-01-23 |
Yasutaka Higa |
Redefine some functions DeltaM in agda
|
2015-01-23 |
Yasutaka Higa |
Change monad definition on DeltaM. use mu.
|
2015-01-21 |
Yasutaka Higa |
Trying Monad-laws for DeltaM
|
2015-01-20 |
Yasutaka Higa |
Update Natural Transformation definitions
|
2015-01-20 |
Yasutaka Higa |
Unify Levels in delta
|
2015-01-19 |
Yasutaka Higa |
Fix implicit values in deltaM-mu
|
2015-01-19 |
Yasutaka Higa |
Rewrite monad definitions for delta/deltaM
|
2015-01-19 |
Yasutaka Higa |
Prove functor-laws for deltaM
|
2015-01-19 |
Yasutaka Higa |
Prove preserve-id for deltaM
|
2015-01-19 |
Yasutaka Higa |
Prove deltaM-preserve-id by mono
|
2015-01-19 |
Yasutaka Higa |
Unify levels on data type. only use suc to proofs
|
2015-01-19 |
Yasutaka Higa |
Defining DeltaM in Agda...
|
2015-01-19 |
Yasutaka Higa |
Split monad-proofs into delta.monad
|
2015-01-19 |
Yasutaka Higa |
Split functor-proofs into delta.functor
|
2015-01-18 |
Yasutaka Higa |
Add record definitions. functor, natural-transformation, monad.
|
2015-01-05 |
Yasutaka Higa |
Mini refactors
|
2015-01-04 |
Yasutaka Higa |
Define DeltaWithLog
|
2015-01-04 |
Yasutaka Higa |
Add example for DeltaM
|
2015-01-04 |
Yasutaka Higa |
Define DeltaM. Delta with Monad
|
2015-01-04 |
Yasutaka Higa |
Added tag InfiniteDelta for changeset fc5cd8c50312
|
2014-12-01 |
Yasutaka Higa |
Adjust proofs
InfiniteDelta
|
2014-12-01 |
Yasutaka Higa |
Prove monad-law-4
|
2014-12-01 |
Yasutaka Higa |
Prove monad-law-2, 3
|
2014-12-01 |
Yasutaka Higa |
Split nat definition
|
2014-12-01 |
Yasutaka Higa |
Refactors
|
2014-12-01 |
Yasutaka Higa |
Prove n-tail-add
|
2014-11-30 |
Yasutaka Higa |
Prove monad-law-1
|
2014-11-30 |
Yasutaka Higa |
Proving monad-law-1
|
2014-11-30 |
Yasutaka Higa |
Trying prove infinite-delta. but I think this definition was missed.
|
2014-11-27 |
Yasutaka Higa |
Change prove method. use Int ...
|
2014-11-27 |
Yasutaka Higa |
Change prove method. use Int ...
|
2014-11-27 |
Yasutaka Higa |
Change headDelta definition. return non-delta value
|
2014-11-27 |
Yasutaka Higa |
Trying prove monad-law-1 by another pattern ....
|
2014-11-26 |
Yasutaka Higa |
Trying prove monad-law-1 by another pattern ...
|
2014-11-26 |
Yasutaka Higa |
Trying prove monad-law-1 by another pattern ...
|
2014-11-26 |
Yasutaka Higa |
Trying prove monad-law-1 by another pattern
|
2014-11-26 |
Yasutaka Higa |
Trying prove monad-law-1 ...
|
2014-11-25 |
Yasutaka Higa |
proving monad-law-1 ...
|
2014-11-25 |
Yasutaka Higa |
Trying prove infinite delta by equiv-reasoning
|
2014-11-24 |
Yasutaka Higa |
Add patterns generator
|
2014-11-22 |
Yasutaka Higa |
Expand pattern-matches...
|
2014-11-22 |
Yasutaka Higa |
Define bind and mu for Infinite Delta
|
2014-11-22 |
Yasutaka Higa |
Mini fixes
|
2014-11-22 |
Yasutaka Higa |
ReDefine Delta used non-empty-list for infinite changes
|
2014-11-19 |
Yasutaka Higa |
Trying redefine monad-laws-1
|
2014-11-19 |
Yasutaka Higa |
Redefine Delta for infinite changes in Agda
|
2014-11-19 |
Yasutaka Higa |
Trying redefine delta for infinite changes
|
2014-11-19 |
Yasutaka Higa |
Adjust function name
|
2014-11-19 |
Yasutaka Higa |
Define Delta for Infinite changes in Haskell
|
2014-11-19 |
Yasutaka Higa |
Fix typo
|
2014-11-19 |
Yasutaka Higa |
Added tag PairDelta for changeset 0c2d758406b1
|
2014-11-17 |
Yasutaka Higa |
Wrote bubble sort with modified calculate
|
2014-11-17 |
Yasutaka Higa |
Wrote >>= style bubble sort
|
2014-11-11 |
Yasutaka Higa |
Implement bubble sort by delta
|
2014-11-11 |
Yasutaka Higa |
Define bubble sort
|
2014-11-09 |
Yasutaka Higa |
Mini refactor
PairDelta
|
2014-11-09 |
Yasutaka Higa |
Define pretty-print for Delta
|
2014-11-01 |
Yasutaka Higa |
Rename to Delta from Similar
|
2014-10-24 |
Yasutaka Higa |
Proof Monad-law-3 (haskell)
|
2014-10-19 |
Yasutaka Higa |
Proof monad-law-h-2, trying monad-law-h-3
|
2014-10-19 |
Yasutaka Higa |
Add Haskell style Monad-laws and Proof Monad-laws-h-1
|
2014-10-19 |
Yasutaka Higa |
Add Comments
|
2014-10-19 |
Yasutaka Higa |
Proof Functor-laws
|
2014-10-19 |
Yasutaka Higa |
Use level in basic/list
|
2014-10-18 |
Yasutaka Higa |
Proof Monad-law-4
|
2014-10-18 |
Yasutaka Higa |
Proof Monad-law-2-2
|
2014-10-18 |
Yasutaka Higa |
Proof Monad-law-2-1
|
2014-10-18 |
Yasutaka Higa |
Proof Monad-law 1
|
2014-10-18 |
Yasutaka Higa |
Expand monad-law 1
|
2014-10-18 |
Yasutaka Higa |
Proof list-associative
|
2014-10-07 |
Yasutaka Higa |
Expand monad-law-1
|
2014-10-07 |
Yasutaka Higa |
Apply level to some functions
|
2014-10-07 |
Yasutaka Higa |
Split basic functions to file
|
2014-10-07 |
Yasutaka Higa |
Define Monad-law 1-4
|
2014-10-07 |
Yasutaka Higa |
Define Similar in Agda
|
2014-10-07 |
Yasutaka Higa |
Define List in Agda
|
2014-10-07 |
Yasutaka Higa |
Update hgignore
|
2014-09-30 |
Yasutaka Higa |
Define similar constructor for different element
|
2014-09-26 |
Yasutaka Higa |
Imporve Similar definition. delete "Single" constructor
|
2014-09-23 |
Yasutaka Higa |
Define Similar sample
|
2014-09-23 |
Yasutaka Higa |
Define Similar as Applicative
|
2014-09-22 |
Yasutaka Higa |
Define Similar as Monad by mu
|
2014-09-22 |
Yasutaka Higa |
Try define Similar as Monad
|
2014-09-09 |
Yasutaka Higa |
Define Similar as Applicative
|
2014-09-09 |
Yasutaka Higa |
Improve mu definition
|
2014-09-06 |
Yasutaka Higa |
Similar as Monad
|
2014-09-06 |
Yasutaka Higa |
Define fmap and mu
|
2014-09-06 |
Yasutaka Higa |
Redefine Similar. reject function in data
|
2014-09-02 |
Yasutaka Higa |
Rename Similer -> Similar
|
2014-09-02 |
Yasutaka Higa |
Define sample for Monad style
|
2014-09-02 |
Yasutaka Higa |
Define Monad style Similer
|
2014-09-02 |
Yasutaka Higa |
Show ErrorMessage
|
2014-09-02 |
Yasutaka Higa |
Define similer function
|
2014-09-02 |
Yasutaka Higa |
Ignore .swp
|
2014-09-02 |
Yasutaka Higa |
Define samples
|
2014-09-02 |
Yasutaka Higa |
Rename some functions
|
2014-09-02 |
Yasutaka Higa |
Define Similer example as Functor
|
2014-08-31 |
Yasutaka Higa |
Define >>= for Similer
|
2014-08-31 |
Yasutaka Higa |
Reduce definition
|
2014-08-31 |
Yasutaka Higa |
Force Implement mu
|
2014-08-31 |
Yasutaka Higa |
Initial commit. define to Functor for Similer
|