GAPPA(1)

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