Hi,
My current proof obligation looks something like this
1 subgoal:
> val it =
w2n (n2w (w2n (cv << dimindex (:i2) !! cv))) = 0
------------------------------------
0. (1 -- 1) add_in = 0w
1. (0 -- 0) add_in = 0w
2. Abbrev (cv = w2w 0w)
: goalstack
Now I would assume that doing something like
e (PURE_REWRITE_TAC[n2w_w2n]);
should reduce the goal to
w2n (cv << dimindex (:i2) !! cv) = 0
---------------------------------------------------
0. (1 -- 1) add_in = 0w
1. (0 -- 0) add_in = 0w
2. Abbrev (cv = w2w 0w)
: goalstack
Now if I am seeing things correctly, the rewrite should happen without a
hitch. However that has not been the case, and that is gating me from
discharging this goal, which looks trivial.
Thank you in advance,
Nikhil
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
