Julien Puydt (May 25 2023 at 07:16): Julien Puydt (May 25 2023 at 07:16):I know about the Fail and Succeed commands -- but they all have a failure case -- either the success or the failure of the child sentence.
I have some OCaml code generating Coq expressions, and until now, they might not even typecheck correctly, so until this code is able to output "Check whatever." or "Fail Check whatever.", I would like it to just output "Try Check whatever.", so compiling the resulting Coq file gives informative output.
Is something like this available?
Gaëtan Gilbert (May 25 2023 at 07:23):no
Last updated: Oct 04 2023 at 22:01 UTC