Stream: math-comp users

Topic: ✔ Error: ssr_have was not found in the current environment


view this post on Zulip Mukesh Tiwari (Jan 20 2023 at 10:05):

Hi everyone,

One of my colleague has asked me if the 'ssr_have' tactic has been deprecated from the recent Mathcomp/Ssreflect library? If yes, what is the replacement? (I see the have tactic used for forward reasoning and my hunch is ssr_have would also have same behaviour but it would be nice there is someone, more expert than me , has a definitive answer).

Edit: nevermind. I was able to solve it.

view this post on Zulip Notification Bot (Jan 20 2023 at 11:25):

Mukesh Tiwari has marked this topic as resolved.


Last updated: Jul 23 2024 at 20:01 UTC