Gears Agda による
Left Learning Red Black Tree の検証

Uechi Yuto, Shinji Kono 琉球大学

Page 1 of 29

研究目的

``` sample1 : (A : Set ) → Set sample1 a = a sample2 : (A : Set ) → (B : Set ) → Set sample2 a b = b ```

findは全部書いても大丈夫そう

これは途中省略してよさそう

t-leaf はコンストラクタ コードの解説 省略した方がたぶん絶対良い right と left なんかはほとんど対照的なので省略とかでよさそう あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう

Keyの比較が入っているから

英語版も欲しい