table of contents
GAPPA(1) | User Commands | GAPPA(1) |
NAME¶
Gappa - manual page for Gappa 1.4.1
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
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
August 2022 | Gappa 1.4.1 |