.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.49.2.
.TH GAPPA "1" "August 2022" "Gappa 1.4.1" "User Commands"
.SH NAME
Gappa \- manual page for Gappa 1.4.1
.SH SYNOPSIS
.B gappa
[\fI\,OPTIONS\/\fR] [\fI\,FILE\/\fR]
.SH DESCRIPTION
Read a statement on standard input and display its proof on standard output.
.TP
\fB\-h\fR, \fB\-\-help\fR
display this help and exit
.TP
\fB\-v\fR, \fB\-\-version\fR
output version information and exit
.SS "Engine parameters:"
.TP
\fB\-Eprecision\fR=\fI\,int\/\fR
internal precision (default: 60)
.TP
\fB\-Edichotomy\fR=\fI\,int\/\fR
dichotomy depth (default: 100)
.TP
\fB\-E[no\-]reverted\-fma\fR
change fma(a,b,c) from a*b+c to c+a*b
.TP
\fB\-Echange\-threshold\fR=\fI\,float\/\fR
threshold for new results (default: 0.01)
.TP
\fB\-Eno\-auto\-dichotomy\fR
do not choose a term for automatic splitting
.SS "Engine modes:"
.TP
\fB\-Munconstrained\fR
do not check for theorem constraints
.TP
\fB\-Mstatistics\fR
display statistics
.TP
\fB\-Mschemes\fR[=\fI\,FILE\/\fR]
produce a dot graph (default: schemes.dot)
.PP
Warnings: (default: all)
.HP
\fB\-W[no\-]dichotomy\-failure\fR
.HP
\fB\-W[no\-]hint\-difference\fR
.HP
\fB\-W[no\-]null\-denominator\fR
.HP
\fB\-W[no\-]unbound\-variable\fR
.SS "Backend:"
.TP
\fB\-Bnull\fR
do not generate a proof (default)
.TP
\fB\-Bcoq\fR
produce a script for Coq
.TP
\fB\-Bcoq\-lambda\fR
produce a lambda\-term for Coq
.TP
\fB\-Bholl\fR
produce a script for HOL Light
.TP
\fB\-Blatex\fR
produce a LaTeX text