log

age author description
Sun, 07 Jun 2020 15:44:39 +0900 Shinji KONO ... default tip
Wed, 04 Mar 2020 19:00:29 +0900 ryokka modify
Wed, 04 Mar 2020 17:51:05 +0900 ryokka fix old binary tree
Wed, 26 Feb 2020 19:00:08 +0900 ryokka writing invaliant
Wed, 26 Feb 2020 18:27:54 +0900 ryokka add new BinaryTree
Mon, 20 Jan 2020 18:12:31 +0900 ryokka fix
Thu, 16 Jan 2020 17:53:47 +0900 ryokka ...
Thu, 16 Jan 2020 16:04:59 +0900 ryokka fix
Wed, 15 Jan 2020 20:50:50 +0900 ryokka add comment
Sat, 07 Dec 2019 08:50:54 +0900 kono bt-replace-hoare
Fri, 06 Dec 2019 18:19:24 +0900 ryokka fix
Fri, 06 Dec 2019 17:48:18 +0900 Shinji KONO use <=
Fri, 06 Dec 2019 17:39:37 +0900 Shinji KONO ...
Fri, 06 Dec 2019 13:01:53 +0900 Shinji KONO minor fix
Thu, 05 Dec 2019 20:38:54 +0900 ryokka add data bt', and some function
Thu, 05 Dec 2019 18:11:22 +0900 ryokka add insert code
Wed, 04 Dec 2019 15:42:47 +0900 ryokka isolate search function problem, and add hoareBinaryTree.agda.
Thu, 07 Nov 2019 21:08:14 +0900 ryokka Add 'non inductiove record' tree, findT, replaceT, and insertT
Sun, 03 Nov 2019 09:27:51 +0900 Shinji KONO ...
Sun, 03 Nov 2019 08:53:00 +0900 Shinji KONO add replaceNode
Sat, 02 Nov 2019 19:33:37 +0900 Shinji KONO ...
Sat, 02 Nov 2019 19:23:10 +0900 Shinji KONO ...
Sat, 02 Nov 2019 18:08:26 +0900 Shinji KONO ...
Sat, 02 Nov 2019 17:34:46 +0900 Shinji KONO ...
Sat, 02 Nov 2019 16:37:27 +0900 Shinji KONO use list base simple stack
Fri, 01 Nov 2019 20:02:55 +0900 ryokka modify findNode1
Fri, 01 Nov 2019 19:12:52 +0900 ryokka Temporary Push
Fri, 01 Nov 2019 17:42:51 +0900 ryokka push local rbtree
Thu, 16 Aug 2018 18:22:08 +0900 ryokka add queue.agda
Sun, 06 May 2018 19:35:38 +0900 Shinji KONO ...
Fri, 27 Apr 2018 19:53:44 +0900 Shinji KONO use lemma5 to follow stack
Fri, 27 Apr 2018 19:19:40 +0900 Shinji KONO add more detail
Thu, 26 Apr 2018 20:09:55 +0900 ryokka separate clearStack
Tue, 17 Apr 2018 10:14:16 +0900 Shinji KONO separate trichotomos exercise
Tue, 17 Apr 2018 10:02:12 +0900 Shinji KONO lemma3
Tue, 17 Apr 2018 09:44:06 +0900 Shinji KONO lemma1 done
Sat, 14 Apr 2018 16:33:16 +0900 Shinji KONO use ⊥-elim (neq refl)
Wed, 11 Apr 2018 11:57:41 +0900 Shinji KONO this slightly better
Wed, 11 Apr 2018 11:29:57 +0900 Shinji KONO using strict total order
Fri, 30 Mar 2018 11:09:06 +0900 Shinji KONO minor fix
Fri, 30 Mar 2018 10:52:51 +0900 Shinji KONO dec ≤′ done
Fri, 30 Mar 2018 10:17:07 +0900 Shinji KONO trichotomos on ≤′ done
Thu, 29 Mar 2018 20:23:51 +0900 Shinji KONO compareTri5 done
Thu, 29 Mar 2018 19:38:49 +0900 ryokka ...
Thu, 29 Mar 2018 18:38:40 +0900 Shinji KONO fix
Thu, 29 Mar 2018 10:58:41 +0900 Shinji KONO some try ..
Tue, 27 Mar 2018 09:30:49 +0900 Shinji KONO add some lemma
Mon, 26 Mar 2018 23:44:02 +0900 Shinji KONO a little fix on refl
Mon, 26 Mar 2018 23:22:07 +0900 Shinji KONO use another nat comparator
Mon, 26 Mar 2018 17:50:04 +0900 ryokka add compareTri
Thu, 18 Jan 2018 10:38:55 +0900 Shinji KONO ...
Wed, 17 Jan 2018 18:28:25 +0900 Shinji KONO fix findNode
Wed, 17 Jan 2018 17:31:41 +0900 Shinji KONO root = Nothing case passed on putTest1
Tue, 16 Jan 2018 17:14:29 +0900 Shinji KONO add some
Sun, 14 Jan 2018 17:57:38 +0900 Shinji KONO compareN x x = EQ
Sun, 14 Jan 2018 08:38:46 +0900 Shinji KONO compare2
Fri, 12 Jan 2018 19:08:29 +0900 ryokka add putTest1Lemma1, putTest1
Fri, 12 Jan 2018 18:30:05 +0900 ryokka add someTest
Thu, 11 Jan 2018 18:54:56 +0900 ryokka add reference
Thu, 11 Jan 2018 17:53:03 +0900 ryokka fix use SingleLinkedStack