GAPPA

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