log

age author description
2021-11-03 Shinji KONO ...
2021-11-03 Shinji KONO with Hoare condition
2021-11-03 Shinji KONO define invariant
2021-11-03 Shinji KONO new approach
2021-11-02 Shinji KONO add fig
2020-06-07 Shinji KONO ...
2020-03-04 ryokka modify
2020-03-04 ryokka fix old binary tree
2020-02-26 ryokka writing invaliant
2020-02-26 ryokka add new BinaryTree
2020-01-20 ryokka fix
2020-01-16 ryokka ...
2020-01-16 ryokka fix
2020-01-15 ryokka add comment
2019-12-06 kono bt-replace-hoare
2019-12-06 ryokka fix
2019-12-06 Shinji KONO use <=
2019-12-06 Shinji KONO ...
2019-12-06 Shinji KONO minor fix
2019-12-05 ryokka add data bt', and some function
2019-12-05 ryokka add insert code
2019-12-04 ryokka isolate search function problem, and add hoareBinaryTree.agda.
2019-11-07 ryokka Add 'non inductiove record' tree, findT, replaceT, and insertT
2019-11-03 Shinji KONO ...
2019-11-02 Shinji KONO add replaceNode
2019-11-02 Shinji KONO ...
2019-11-02 Shinji KONO ...
2019-11-02 Shinji KONO ...
2019-11-02 Shinji KONO ...
2019-11-02 Shinji KONO use list base simple stack
2019-11-01 ryokka modify findNode1
2019-11-01 ryokka Temporary Push
2019-11-01 ryokka push local rbtree
2018-08-16 ryokka add queue.agda
2018-05-06 Shinji KONO ...
2018-04-27 Shinji KONO use lemma5 to follow stack
2018-04-27 Shinji KONO add more detail
2018-04-26 ryokka separate clearStack
2018-04-17 Shinji KONO separate trichotomos exercise
2018-04-17 Shinji KONO lemma3
2018-04-17 Shinji KONO lemma1 done
2018-04-14 Shinji KONO use ⊥-elim (neq refl)
2018-04-11 Shinji KONO this slightly better
2018-04-11 Shinji KONO using strict total order
2018-03-30 Shinji KONO minor fix
2018-03-30 Shinji KONO dec ≤′ done
2018-03-30 Shinji KONO trichotomos on ≤′ done
2018-03-29 Shinji KONO compareTri5 done
2018-03-29 ryokka ...
2018-03-29 Shinji KONO fix
2018-03-29 Shinji KONO some try ..
2018-03-27 Shinji KONO add some lemma
2018-03-26 Shinji KONO a little fix on refl
2018-03-26 Shinji KONO use another nat comparator
2018-03-26 ryokka add compareTri
2018-01-18 Shinji KONO ...
2018-01-17 Shinji KONO fix findNode
2018-01-17 Shinji KONO root = Nothing case passed on putTest1
2018-01-16 Shinji KONO add some
2018-01-14 Shinji KONO compareN x x = EQ