GitLab

Optional and named arguments

Optional and named arguments in functions signature.
For optional/named arguments in application it requires some more
work around the printer.

Theory seq.OfList: refactoring

Code refactoring.

Check if the refinement record type possesses all the fields
(same name, same type, same ghost status) included in the
refined type.

Avoid inlining proxy variables whenever there are conflicting effects

Not inlining proxy variables inside a [Efun].

Extraction of let x = e1 in e2

Fold_left for lists and sequences (wip)

Not printing parentheses around constants
(though still not completely satisfying

Optimization of proxy variables.

Why3 files from standard library are not extracted

Optimization of singleton record types.
Still missing treatment of record types defined in drivers