Stream: Coq users

Topic: use of destruct command


view this post on Zulip pianke (Mar 23 2023 at 10:29):

Function f requires two arguments and gives true or false. When i apply destruct command then first case is being consider but it is not visible in hypothesis. I wan to see it in hypothesis. I have applied destruct f a b as eq1 so that it look like f a b=true first time (then f a b=false in hypothesis) but it does not work.

view this post on Zulip Guillaume Melquiond (Mar 23 2023 at 10:50):

Syntax is destruct (f a b) eqn:eq1.

view this post on Zulip pianke (Mar 23 2023 at 10:58):

Thank you for correction.


Last updated: Jun 16 2024 at 02:41 UTC