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.
Mukesh Tiwari has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC