<div dir="ltr">Hi, Agda list.<br><br>I would like to share some code with you. Binary tree enumeration procedure is defined and verified. It is typical combinatorial problem, and I just wondered how hard it could be to define and reason about it in Agda. As far as I know, it hasn't been done before. Please, let me know if it's not so. <br>
<br>It is available here: <a href="https://github.com/zhyltsovd/agda-btree-enumeration">https://github.com/zhyltsovd/agda-btree-enumeration</a> <br><br>I hope somebody finds it useful.<br>All improvement suggestions are welcomed.<br>
</div>