NAME
Gappa - manual page for Gappa 1.6.0
SYNOPSIS
gappa [OPTIONS] [FILE]
DESCRIPTION
Read a statement on standard input and display its proof on standard output.
- -h, --help
-
display this help and exit
- -v, --version
-
output version information and exit
- -d, --debug
-
print debug information while gappa is running
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