NAME

       Gappa - manual page for Gappa 1.5.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

Gappa 1.5.0                                       January 2025                                          GAPPA(1)