   (equal args 'fstar-subp-prover-args-for-compiler-hacking))
 
 (defcustom fstar-subp-prover-args nil
-  "Used for computing arguments to pass to F* in interactive mode.
+  "Arguments to pass to F* in interactive mode.
 
 If set to a string, that string is considered to be a single
 argument to pass to F*.  If set to a list of strings, each element

  "Find path to SMT solver executable."
  (fstar-find-executable fstar-smt-executable "SMT solver" 'fstar-smt-executable))

(defun fstar-subp--parse-prover-args ()
  "Translate `fstar-subp-prover-args' into a list of strings."
  (let ((args (fstar--resolve-fn-value fstar-subp-prover-args)))
    (cond ((listp args) args)
          ((stringp args) (list args))
          (t (user-error "Interpreting `fstar-subp-prover-args' \
led to invalid value [%s]" args)))))

(defun fstar-subp-get-prover-args ()
  "Compute F*'s arguments.
Function is public to make it easier to debug `fstar-subp-prover-args'."
  (let ((smt-path (fstar--maybe-cygpath (fstar-subp-find-smt-solver)))
        (usr-args (fstar-subp--parse-prover-args))
        (ide-flag (if (fstar--has-feature 'json-subp) "--ide" "--in")))
    `(,(fstar-subp--buffer-file-name) ,ide-flag "--smt" ,smt-path ,@usr-args)))

(defun fstar-subp--prover-includes-for-compiler-hacking ()

Some examples (see below about `…'):

- (setq fstar-subp-prover-args \"--ab\") results in F* being
called as ‘fstar.exe … --ab …’.

- (setq fstar-subp-prover-args \\='(\"--ab\" \"--cd\")) results in
F* being called as ‘fstar.exe … --ab --cd …’.

- (setq fstar-subp-prover-args (lambda () \\='(\"--ab\" \"--cd\")))
results in F* being called as ‘fstar.exe … --ab --cd …’.

In addition to these flags, `fstar-mode' always includes (as
indicated above by the first `…') both \\='--smt <path-to-z3>\\='
and one of \\='--ide\\=' and \\='--in\\=', and any flags computed
from `fstar-subp-prover-additional-args' (as indicated above by
the second `…').

To debug unexpected behaviors with this variable, try
evaluating (fstar-subp-get-prover-args).  Note that passing
