Mercurial > hg > Gears > GearsAgda

comparison Todo.txt @ 573:8777baeb90f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 May 2018 19:35:38 +0900
parents 7d9af1d4b5af
children 73fc32092b64
comparison
equal deleted inserted replaced
572:eb75d9971451 573:8777baeb90f8
1 Sun May 6 17:54:50 JST 2018
2
3 do1 a $ \b -> do2 b next を、do1 と do2 に分離することはできる?
4
5
6 Mon Apr 30 17:15:16 JST 2018
7
8 Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない
9 やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい
10
1 Mon Mar 26 17:43:06 JST 2018 11 Mon Mar 26 17:43:06 JST 2018
2 12
3 Decidable を使って Compare の場合分けを行う 13 Decidable を使って Compare の場合分けを行う
4 Decidable を使うと Eq から x ≡ y の証明を取り出すことができる 14 Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
5 場合分けには Trichotomous を使う 15 場合分けには Trichotomous を使う
6 compareTri を完成させる 16 compareTri を完成させる Done
7 17
8 Fri Jan 5 16:43:26 JST 2018 18 Fri Jan 5 16:43:26 JST 2018
9 19
10 unbalanced binary search tree の動作を調べる 20 unbalanced binary search tree の動作を調べる
11 21