I am pleased to release version 1.2 of InvarGenT, a system that infers invariants and postconditions, and exports the corresponding GADTs-based OCaml code.
https://github.com/lukstafi/invargent/releases

The highlight of this release is the AVL trees example see:
https://github.com/lukstafi/invargent/blob/master/examples/avl_tree.gadt
https://github.com/lukstafi/invargent/blob/master/examples/avl_tree.gadti.target
InvarGenT finds out that the height of a rotated tree can be the same as original tree or one bigger, the same fact for the tree with added element, that the height of merger of two trees is at most one bigger than that of the larger tree, and that removing an element can decrease the height of a tree, by at most 1.

Changes:
* Several bug fixes.
* So-called "opti" relations: "k=min(m,n)" and "k=max(m,n)" in the numerical sort.
* So-called "subopti" relations "k<=max(m,n)" and "min(m,n)<=k" in the numerical sort.
* Less confusing syntax for existential types, "datatype" and "datacons" keywords.
* Pattern-matching guards "when e1 <= e2", where e1 and "e2 are expressions of type "Num".
* Positive assert clauses, "assert num e1 <= e2; ..." and "assert type e1 = e2; ...".
* Flagship example: AVL trees with imbalance of 2 (based on the implementation from OCaml standard library).