Stream: Coq users

Topic: ✔ How to do induction?


view this post on Zulip Julin Shaji (Feb 16 2024 at 07:32):

I used to think pose proof was bad style. But I guess have is often used. Thanks.

view this post on Zulip Julin Shaji (Feb 16 2024 at 07:33):

The oneliners made me look up syntax. Got to know some new bits (and some like ? is yet to be looked up.. :D)

view this post on Zulip Notification Bot (Feb 16 2024 at 07:35):

Julin Shaji has marked this topic as resolved.

view this post on Zulip Ana de Almeida Borges (Feb 22 2024 at 14:16):

Julin Shaji said:

The oneliners made me look up syntax. Got to know some new bits (and some like ? is yet to be looked up.. :D)

The ? is a way to let Coq pick a name for the term being introduced. It's anti-recommended unless the term in question is not going to survive the end of the line, like in this case.

view this post on Zulip Paolo Giarrusso (Feb 22 2024 at 19:51):

That seems stricter than I've seen in many projects, but the proof script is definitely not supposed to mention the generated name


Last updated: Jun 13 2024 at 19:02 UTC