fstar-experiments

several experiments on F * for the generation of (almost) automatic proofs

todo :

1. AVL tree (done)
2. Set and Map module (done)
3. Binary Decision Diagram (done)

the final version is in BDD.fst, BDD2.fst is an incomplete attempt of typed BDD, difficult because several typed BDD can represent the same function