二分木の Hoare Logic

いつもの Agda で格闘中。なんか、実は

　割と簡単で、2018の方法でできていた

という落ちが。仕様の受け方が間違ってて、継続の入力で受ければ良いだけだった。

　test = next ( λ x → x ≡ c10 )

みたいに書くのではなくて、

　spec : (x : Nat) → x ≡ c10 → t
test = next spec

みたいに書けばよいだけだったらしい。

二分木の方は「これでできた」「だめだ」ループを20回くらい回ったんですが、

　どうも、結局、condition ではなくて、二分木に値が入っているという意味を表すデータ構造

つまり、表示的意味なデータ構造を書いてしまうのが良いらしい。そんなもんらしいです。