Mercurial > hg > Gears > GearsAgda

diff Todo.txt @ 573:8777baeb90f8
...
author: Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date: Sun, 06 May 2018 19:35:38 +0900
parents: 7d9af1d4b5af
children: 73fc32092b64
--- a/Todo.txt	Fri Apr 27 19:53:44 2018 +0900
+++ b/Todo.txt	Sun May 06 19:35:38 2018 +0900
@@ -1,9 +1,19 @@
+Sun May  6 17:54:50 JST 2018
+
+    do1 a $ \b ->  do2 b next を、do1 と do2  に分離することはできる?
+
+
+Mon Apr 30 17:15:16 JST 2018
+
+    Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない
+    やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい
+
 Mon Mar 26 17:43:06 JST 2018
 
-    Decidable を使って Compare の場合分けを行う
+    Decidable を使って Compare の場合分けを行う    
     Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
     場合分けには Trichotomous を使う
-    compareTri を完成させる               
+    compareTri を完成させる    Done
 
 Fri Jan  5 16:43:26 JST 2018
author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 06 May 2018 19:35:38 +0900
parents	7d9af1d4b5af
children	73fc32092b64