Engine parameters:¶

-Eprecision=int

internal precision (default: 60)

-Edichotomy=int

dichotomy depth (default: 100)

-E[no-]reverted-fma

change fma(a,b,c) from a*b+c to c+a*b

-Echange-threshold=float

threshold for new results (default: 0.01)

-Eno-auto-dichotomy

do not choose a term for automatic splitting

Engine modes:¶

-Munconstrained

do not check for theorem constraints

-Mstatistics

display statistics

-Mschemes[=FILE]

produce a dot graph (default: schemes.dot)

Warnings: (default: all)

-W[no-]dichotomy-failure

-W[no-]hint-difference

-W[no-]null-denominator

-W[no-]unbound-variable

Backend:¶

-Bnull

do not generate a proof (default)

-Bcoq

produce a script for Coq

-Bcoq-lambda

produce a lambda-term for Coq

-Bholl

produce a script for HOL Light

-Blatex

produce a LaTeX text

-Bd2

produce a D2 graph file