Stream: Coq users

Topic: Curly brace in ssreflect


view this post on Zulip Julin Shaji (Mar 23 2024 at 04:38):

Hi. What does the curly braces in this syntax mean?

elim => {p q}

Found this
https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/ssreflect-proof-language.html#clear-switch

But still didn't get what it does.

Is it that the introduced variables are forgotten after the tactic or something?

view this post on Zulip Julin Shaji (Mar 23 2024 at 07:34):

Okay, I think I got it.
It can be used to clear old variable names. Helpful to reuse that name in sub-goals.


Last updated: Jun 18 2024 at 22:01 UTC