• x + y, x - y, x * y, x / y: add, subtract, multiply, divide; must not divide by zero
• - x: negation
• / x: reciprocal; x must not be zero
• [x, y]: closed interval
• x.[n]: nth closed interval in the sequence defining x; n starts from zero
• x => x * x: function definition
• f x: function application
• let x := 3 in x * x: local variable
• min xs: lower bound of interval xs
• max xs: upper bound of interval xs
• make f: number contained in the rational intervals f(0), f(1), f(2), ...; intervals must be nested and converge to zero width
• intersect f: number contained in the real intervals f(0), f(1), f(2), ...; intervals must be nested and converge to zero width
• repeat f x n: result of applying f to x n times
• round x: result of either rounding x up to the next integer or rounding x down to the previous integer
• piecewise a f g x: yields f(x) when x ≤ a and g(x) when x ≥ a; if f(x) differs from g(x), x must differ from a
• abs x: absolute value

Ignoring a "must" above results in undefined behavior, which may include the calculator hanging or producing incorrect results.

In addition to the main source code, the calculator demo uses code from the following projects:

• Coq [source] [license]
• js_of_ocaml [source] [license]
• Zarith [source] [license]
• Zarith Stubs JS [source] [license]
• BigInteger.js (included in Zarith Stubs JS)

The easiest way to fetch all required dependencies is to install opam and run:

opam install ocaml ocamlfind coq=8.16.0 js_of_ocaml js_of_ocaml-ppx zarith zarith_stubs_js

Then in the directory where you have downloaded the main source code, run:

./extract.sh