strict bounds for BNFs (by Jan van Brügge)

More lemmas.

Centralized some char-related lemmas in distribution.

prefer antiquotations;

clarified modules;

more documentation;

merged

tuned whitespace;

clarified signature: File.read_lines is based on scalable Bytes.T; discontinued somewhat pointless File.fold_lines;

clarified modules;

prefer scalable Bytes.T;

unused;

prefer scalable Bytes.T;

missing recursive let-expansion in SMT translation

merged

added lemma monotone_on_o

redefined mono_on and strict_mono_on as an abbreviation of monotone_on

changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates

more robust CSV syntax, e.g. for "pull_date";

merged

more scalable generated files and code export, using Bytes.T;

more operations;

proper execution of Bytes.write; tuned;

Avoid calculations where not necessary.

Prefer existing horner sum combinator.

Executable lexords.

Less warnings.

merged

more operations;

removed unused operations; tuned (again);