Since why is presently named why3, the zsh functions too

share/zsh/_why

-#compdef why
-##
-## zsh completion for why
-## generated by ocompl
-
-##
-##
-##
-##
-
-local curcontext state line cmds ret=1
-
-##
-_arguments -s -S \
-     '(- *)'{-h,--help}'[Brief help message]' \
-     '-'"[Read the input file from stdin]"\
-     '*-T'"[<theory> Select <theory> in the input file or in the library]:<theory>:"\
-     '*--theory'"[same as -T]:<theory>:"\
-     '*-G'"[<goal> Select <goal> in the last selected theory]:<goal>:"\
-     '*--goal'"[same as -G]:<goal>:"\
-     '-C'"[<file> Read configuration from <file>]:Configuration File:_files  -g '*.conf'"\
-     '--config'"[same as -C]:Configuration File:_files  -g '*.conf'"\
-     "(-L --library -I)"'-L'"[<dir> Add <dir> to the library search path]:Mlpost lib path:_files -/  "\
-     "(-L --library -I)"'--library'"[same as -L]:Mlpost lib path:_files -/  "\
-     "(-L --library -I)"'-I'"[same as -L (obsolete)]:Mlpost lib path (obsolete use -L):_files -/  "\
-     "(-D --driver -P -prover)"'-P'"[<prover> Prove or print (with -o) the selected goals]:<prover>:compadd $(why --list-provers | egrep -E "^  [a-z]"|cut -d' '  -f 3)"\
-     "(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:compadd $(why --list-provers | egrep -E "^  [a-z]"|cut -d' '  -f 3)"\
-     "(-F --format)"'-F'"[<format> Input format (default: \"why\")]:<input format>:"\
-     "(-F --format)"'--format'"[same as -F]:<input format>:"\
-     "(-t --timelimit)"'-t'"[<sec> Set the prover\'s time limit (default=10, no limit=0)]:<timeout s>:"\
-     "(-t --timelimit)"'--timelimit'"[same as -t]:<timeout s>:"\
-     "(-m --memlimit)"'-m'"[<MiB> Set the prover\'s memory limit (default: no limit)]:<memory limit M>:"\
-     "(-m --memlimit)"'--memlimit'"[same as -m]:<memory limit M>:"\
-     "(-D --driver -P -prover)"'-D'"[<file> Specify a prover\'s driver (conflicts with -P)]:Prover\'s driver:_files  -g '*.drv'"\
-     "(-D --driver -P -prover)"'--driver'"[same as -D]:Prover\'s driver:_files  -g '*.drv'"\
-     "(-o --output)"'-o'"[<dir> Print the selected goals to separate files in <dir>]:directory output:_files -/  "\
-     "(-o --output)"'--output'"[same as -o]:directory output:_files -/  "\
-     '--print-theory'"[Print the selected theories]"\
-     '--print-namespace'"[Print the namespaces of selected theories]"\
-     '--list-transforms'"[List the registered transformations]"\
-     '--list-printers'"[List the registered printers]"\
-     '--list-provers'"[List the known provers]"\
-     '--list-formats'"[List the known input formats]"\
-     "(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--parse-only'"[Stop after parsing]"\
-     "(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--type-only'"[Stop after type checking]"\
-     '--debug'"[Set the debug flag]"\
-     '*-a'"[<transformation> Add a transformation to apply to the task]:<transformation>:compadd $(why --list-transforms | grep -e "^  ")"\
-     '*--apply-transform'"[same as -a]:<transformation>:compadd $(why --list-transforms | grep -e "^  ")"\
-     "*:The why file:_files  -g '*.why'" \
-     && ret=0
-
-return ret
-
-_why "$@"