pianke (Mar 23 2023 at 10:29): 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.
Guillaume Melquiond (Mar 23 2023 at 10:50):Syntax is destruct (f a b) eqn:eq1.
pianke (Mar 23 2023 at 10:58):Thank you for correction.
Last updated: Apr 19 2024 at 11:02 UTC