lean4-htt/tests/lean/kernelMVarBug.lean.expected.out at d5e7dbad8071eccf40f2b49ba4145f3799510afe - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

Kyle Miller d5e7dbad80

fix: make "use `set_option diagnostics true" message conditional on current setting (#4781 )

It is confusing that the message suggesting to use the `diagnostics`
option is given even when the option is already set. This PR makes use
of lazy message data to make the message contingent on the option being
false.

It also tones down the promise that there is any diagonostic information
available, since sometimes there is nothing to report.

Suggested by Johan Commelin.

2024-07-31 03:53:09 +00:00

3 lines

177 B

Text

Raw Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
   HAdd α α α
 Additional diagnostic information may be available by using the `set_option diagnostics true` command.