Stream: Coq users

Topic: Commands Fail and Succeed

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (May 25 2023 at 07:23):


Last updated: Oct 04 2023 at 22:01 UTC