BTree feedback

Stream: lean4

[Chris B]

I wrote a BTree using a description in the comments of Rust's BTreeMap implementation along the lines of "this is what we'd do if we had dependent types", where the nodes have their height as a type parameter. If anyone is willing to take a look and offer criticism/advice/feedback I would appreciate it. The file is long, but you'll have the idea by line 30 : https://gist.github.com/ammkrn/d7212abd94dfb86308647c888ca23ac0

The biggest thing I feel like I don't have a good answer for is reducing the need to match on the height. It seems like the alternative is, for functions that are not recursive, to have two implementations, one for height 0, one for height h+1, and then call properly from the parent where the match has already been done. That ended up getting sort of verbose, and it you lose some niceties; it doesn't seem like there's a way to have e.g. Leaf.getField for Node K V 0 and InternalNode.getField for Node K V (h+1), and have them work as dot notation after doing a dependent match.