Hi,
I want to prove a goal like this:
`case d of u =1 |s =2|d =3
|p =4`
Is there a tactic which can match d with the branch d and then execute this
branch.--
On 04/11/14 13:33, ＂f~鳓ぁぇ wrote:
Hi,
I want to prove a goal like this:
`case d of u =1 |s =2|d
=3
|p =4`
Is there a tactic which can match d with the branch d and then execute
this
branch.
SIMP_TAC (srw_ss()) []
or
SRW_TAC[][]
should
Hi,
if you don't like stateful tactics, you should also have a look at the
library DatatypeSimps. Moreover, it often helps me to turn off pretty
printing of case-expressions via
set_trace pp_cases 0
You need rewriting of the list_CASE and equality of chars. So, your
goal should also be solved
