# fstar.exe
# auto-generated from output of `fstar.exe --help`
# using FStar/.scripts/fstar_fish_completions.py
complete -c fstar.exe -l abort_on --description "non-negative integer  Abort on the n-th error or warning raised. Useful in combination with --trace_error. Count starts at 1, use 0 to disable. (default 0)"
complete -c fstar.exe -l admit_smt_queries -r --description "Admit SMT queries, unsafe! (default 'false')"
complete -c fstar.exe -l admit_except -r --description "Admit all queries, except those with label (<symbol>, <id>)) (e.g. --admit_except '(FStar.Fin.pigeonhole, 1)' or --admit_except FStar.Fin.pigeonhole)"
complete -c fstar.exe -l already_cached --description "One or more space-separated occurrences of '[+|-]( * | namespace | module)'"
complete -c fstar.exe -l cache_checked_modules --description "Write a '.checked' file for each module after verification and read from it if present, instead of re-verifying"
complete -c fstar.exe -l cache_dir --description "dir  Read and write .checked and .checked.lax in directory <dir>"
complete -c fstar.exe -l cache_off --description "Do not read or write any .checked files"
complete -c fstar.exe -l print_cache_version --description "Print the version for .checked files and exit."
complete -c fstar.exe -l cmi --description "Inline across module interfaces during extraction (aka. cross-module inlining)"
complete -c fstar.exe -l codegen -r --description "Generate code for further compilation to executable code, or build a compiler plugin"
complete -c fstar.exe -l codegen-lib --description "namespace  External runtime library (i.e. M.N.x extracts to M.N.X instead of M_N.x)"
complete -c fstar.exe -l debug -r --description "Control the verbosity of debugging info"
complete -c fstar.exe -l defensive -r --description "Enable several internal sanity checks, useful to track bugs and report issues."
complete -c fstar.exe -l dep -r --description "Output the transitive closure of the full dependency graph in three formats:"
complete -c fstar.exe -l detail_errors --description "Emit a detailed error report by asking the SMT solver many queries; will take longer"
complete -c fstar.exe -l detail_hint_replay --description "Emit a detailed report for proof whose unsat core fails to replay"
complete -c fstar.exe -l dump_module --description "module_name"
complete -c fstar.exe -l eager_subtyping --description "Try to solve subtyping constraints at each binder (loses precision but may be slightly more efficient)"
complete -c fstar.exe -l extract --description "One or more space-separated occurrences of '[+|-]( * | namespace | module)'"
complete -c fstar.exe -l extract_module --description "module_name  Deprecated: use --extract instead; Only extract the specified modules (instead of the possibly-partial dependency graph)"
complete -c fstar.exe -l extract_namespace --description "namespace name  Deprecated: use --extract instead; Only extract modules in the specified namespace"
complete -c fstar.exe -l expose_interfaces --description "Explicitly break the abstraction imposed by the interface of any implementation file that appears on the command line (use with care!)"
complete -c fstar.exe -l hide_uvar_nums --description "Don't print unification variable numbers"
complete -c fstar.exe -l hint_dir --description "path  Read/write hints to <dir>/module_name.hints (instead of placing hint-file alongside source file)"
complete -c fstar.exe -l hint_file --description "path  Read/write hints to <path> (instead of module-specific hints files; overrides hint_dir)"
complete -c fstar.exe -l hint_info --description "Print information regarding hints (deprecated; use --query_stats instead)"
complete -c fstar.exe -l in --description "Legacy interactive mode; reads input from stdin"
complete -c fstar.exe -l ide --description "JSON-based interactive mode for IDEs"
complete -c fstar.exe -l lsp --description "Language Server Protocol-based interactive mode for IDEs"
complete -c fstar.exe -l include --description "path  A directory in which to search for files included on the command line"
complete -c fstar.exe -l print --description "Parses and prettyprints the files included on the command line"
complete -c fstar.exe -l print_in_place --description "Parses and prettyprints in place the files included on the command line"
complete -c fstar.exe -l force --description "Force checking the files given as arguments even if they have valid checked files"
complete -c fstar.exe -l fuel --description "non-negative integer or pair of non-negative integers  Set initial_fuel and max_fuel at once"
complete -c fstar.exe -l ifuel --description "non-negative integer or pair of non-negative integers  Set initial_ifuel and max_ifuel at once"
complete -c fstar.exe -l initial_fuel --description "non-negative integer  Number of unrolling of recursive functions to try initially (default 2)"
complete -c fstar.exe -l initial_ifuel --description "non-negative integer  Number of unrolling of inductive datatypes to try at first (default 1)"
complete -c fstar.exe -l keep_query_captions -r --description "Retain comments in the logged SMT queries (requires --log_queries; default true)"
complete -c fstar.exe -l lax --description "Run the lax-type checker only (admit all verification conditions)"
complete -c fstar.exe -l load --description "module  Load compiled module"
complete -c fstar.exe -l log_types --description "Print types computed for data/val/let-bindings"
complete -c fstar.exe -l log_queries --description "Log the Z3 queries in several queries-*.smt2 files, as we go"
complete -c fstar.exe -l max_fuel --description "non-negative integer  Number of unrolling of recursive functions to try at most (default 8)"
complete -c fstar.exe -l max_ifuel --description "non-negative integer  Number of unrolling of inductive datatypes to try at most (default 2)"
complete -c fstar.exe -l MLish --description "Trigger various specializations for compiling the F* compiler itself (not meant for user code)"
complete -c fstar.exe -l no_default_includes --description "Ignore the default module search paths"
complete -c fstar.exe -l no_extract --description "module name  Deprecated: use --extract instead; Do not extract code from this module"
complete -c fstar.exe -l no_location_info --description "Suppress location information in the generated OCaml output (only relevant with --codegen OCaml)"
complete -c fstar.exe -l no_smt --description "Do not send any queries to the SMT solver, and fail on them instead"
complete -c fstar.exe -l normalize_pure_terms_for_extraction --description "Extract top-level pure terms after normalizing them. This can lead to very large code, but can result in more partial evaluation and compile-time specialization."
complete -c fstar.exe -l odir --description "dir  Place output in directory <dir>"
complete -c fstar.exe -l prims --description "file"
complete -c fstar.exe -l print_bound_var_types --description "Print the types of bound variables"
complete -c fstar.exe -l print_effect_args --description "Print inferred predicate transformers for all computation types"
complete -c fstar.exe -l print_expected_failures --description "Print the errors generated by declarations marked with expect_failure, useful for debugging error locations"
complete -c fstar.exe -l print_full_names --description "Print full names of variables"
complete -c fstar.exe -l print_implicits --description "Print implicit arguments"
complete -c fstar.exe -l print_universes --description "Print universes"
complete -c fstar.exe -l print_z3_statistics --description "Print Z3 statistics for each SMT query (details such as relevant modules, facts, etc. for each proof)"
complete -c fstar.exe -l prn --description "Print full names (deprecated; use --print_full_names instead)"
complete -c fstar.exe -l quake --description "positive integer or pair of positive integers  Repeats SMT queries to check for robustness"
complete -c fstar.exe -l quake --description "N/M repeats each query checks that it succeeds at least N out of M times, aborting early if possible"
complete -c fstar.exe -l quake --description "N/M/k works as above, except it will unconditionally run M times"
complete -c fstar.exe -l quake --description "N is an alias for --quake N/N"
complete -c fstar.exe -l quake --description "N/k is an alias for --quake N/N/k"
complete -c fstar.exe -l query_stats --description "Print SMT query statistics"
complete -c fstar.exe -l record_hints --description "Record a database of hints for efficient proof replay"
complete -c fstar.exe -l record_options --description "Record the state of options used to check each sigelt, useful for the `check_with` attribute and metaprogramming"
complete -c fstar.exe -l retry --description "positive integer  Retry each SMT query N times and succeed on the first try. Using --retry disables --quake."
complete -c fstar.exe -l reuse_hint_for --description "toplevel_name  Optimistically, attempt using the recorded hint for <toplevel_name> (a top-level name in the current module) when trying to verify some other term 'g'"
complete -c fstar.exe -l report_assumes -r --description "Report every use of an escape hatch, include assume, admit, etc."
complete -c fstar.exe -l silent --description "Disable all non-critical output"
complete -c fstar.exe -l smt --description "path  Path to the Z3 SMT solver (we could eventually support other solvers)"
complete -c fstar.exe -l smtencoding.elim_box -r --description "Toggle a peephole optimization that eliminates redundant uses of boxing/unboxing in the SMT encoding (default 'false')"
complete -c fstar.exe -l smtencoding.nl_arith_repr -r --description "Control the representation of non-linear arithmetic functions in the SMT encoding:"
complete -c fstar.exe -l smtencoding.l_arith_repr -r --description "Toggle the representation of linear arithmetic functions in the SMT encoding:"
complete -c fstar.exe -l smtencoding.valid_intro -r --description "Include an axiom in the SMT encoding to introduce proof-irrelevance from a constructive proof"
complete -c fstar.exe -l smtencoding.valid_elim -r --description "Include an axiom in the SMT encoding to eliminate proof-irrelevance into the existence of a proof witness"
complete -c fstar.exe -l tactic_raw_binders --description "Do not use the lexical scope of tactics to improve binder names"
complete -c fstar.exe -l tactics_failhard --description "Do not recover from metaprogramming errors, and abort if one occurs"
complete -c fstar.exe -l tactics_info --description "Print some rough information on tactics, such as the time they take to run"
complete -c fstar.exe -l tactic_trace --description "Print a depth-indexed trace of tactic execution (Warning: very verbose)"
complete -c fstar.exe -l tactic_trace_d --description "positive_integer  Trace tactics up to a certain binding depth"
complete -c fstar.exe -l __tactics_nbe --description "Use NBE to evaluate metaprograms (experimental)"
complete -c fstar.exe -l tcnorm -r --description "Attempt to normalize definitions marked as tcnorm (default 'true')"
complete -c fstar.exe -l timing --description "Print the time it takes to verify each top-level definition"
complete -c fstar.exe -l trace_error --description "Don't print an error message; show an exception trace instead"
complete -c fstar.exe -l ugly --description "Emit output formatted for debugging"
complete -c fstar.exe -l unthrottle_inductives --description "Let the SMT solver unfold inductive types to arbitrary depths (may affect verifier performance)"
complete -c fstar.exe -l unsafe_tactic_exec --description "Allow tactics to run external processes. WARNING: checking an untrusted F* file while using this option can have disastrous effects."
complete -c fstar.exe -l use_eq_at_higher_order --description "Use equality constraints when comparing higher-order types (Temporary)"
complete -c fstar.exe -l use_hints --description "Use a previously recorded hints database for proof replay"
complete -c fstar.exe -l use_hint_hashes --description "Admit queries if their hash matches the hash recorded in the hints database"
complete -c fstar.exe -l use_native_tactics --description "path  Use compiled tactics from <path>"
complete -c fstar.exe -l no_plugins --description "Do not run plugins natively and interpret them as usual instead"
complete -c fstar.exe -l no_tactics --description "Do not run the tactic engine before discharging a VC"
complete -c fstar.exe -l using_facts_from --description "One or more space-separated occurrences of '[+|-]( * | namespace | fact id)'"
complete -c fstar.exe -l vcgen.optimize_bind_as_seq --description "[off|without_type|with_type]"
complete -c fstar.exe -l __temp_no_proj --description "module_name  Don't generate projectors for this module"
complete -c fstar.exe -l version --description "Display version number"
complete -c fstar.exe -l warn_default_effects --description "Warn when (a -> b) is desugared to (a -> Tot b)"
complete -c fstar.exe -l z3cliopt --description "option  Z3 command line options"
complete -c fstar.exe -l z3refresh --description "Restart Z3 after each query; useful for ensuring proof robustness"
complete -c fstar.exe -l z3rlimit --description "positive_integer  Set the Z3 per-query resource limit (default 5 units, taking roughtly 5s)"
complete -c fstar.exe -l z3rlimit_factor --description "positive_integer  Set the Z3 per-query resource limit multiplier. This is useful when, say, regenerating hints and you want to be more lax. (default 1)"
complete -c fstar.exe -l z3seed --description "positive_integer  Set the Z3 random seed (default 0)"
complete -c fstar.exe -l use_two_phase_tc -r --description "Use the two phase typechecker (default 'true')"
complete -c fstar.exe -l __no_positivity --description "Don't check positivity of inductive types"
complete -c fstar.exe -l warn_error --description "The [-warn_error] option follows the OCaml syntax, namely:"
complete -c fstar.exe -l use_nbe -r --description "Use normalization by evaluation as the default normalization strategy (default 'false')"
complete -c fstar.exe -l use_nbe_for_extraction -r --description "Use normalization by evaluation for normalizing terms before extraction (default 'false')"
complete -c fstar.exe -l trivial_pre_for_unannotated_effectful_fns -r --description "Enforce trivial preconditions for unannotated effectful functions (default 'true')"
complete -c fstar.exe -l __debug_embedding --description "Debug messages for embeddings/unembeddings of natively compiled terms"
complete -c fstar.exe -l eager_embedding --description "Eagerly embed and unembed terms to primitive operations and plugins: not recommended except for benchmarking"
complete -c fstar.exe -l profile_group_by_decl --description "Emit profiles grouped by declaration rather than by module"
complete -c fstar.exe -l profile_component --description "One or more space-separated occurrences of '[+|-]( * | namespace | module | identifier)'"
complete -c fstar.exe -l profile --description "One or more space-separated occurrences of '[+|-]( * | namespace | module)'"
complete -c fstar.exe -l help --description "Display this information"
