Skip to content

Commit

Permalink
Avoid set skip of NUMERAL
Browse files Browse the repository at this point in the history
This even skips matching numerical constants in rewrite rules,
e.g.,
```
let QLANE = define
 `QLANE reg 8 ix = QREG' reg :> LANE_B ix /\
  QLANE reg 16 ix = QREG' reg :> LANE_H ix /\
  QLANE reg 32 ix = QREG' reg :> LANE_S ix /\
  QLANE reg 64 ix = QREG' reg :> LANE_D ix`;;
```
  • Loading branch information
aqjune-aws committed Feb 28, 2025
1 parent 2ff8dde commit f6321f2
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion arm/proofs/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1014,7 +1014,6 @@ let PURE_DECODE_CONV =
custom_word_compute_add_convs rw;
int_compute_add_convs rw;
num_compute_add_convs rw;
set_skip rw `NUMERAL` (Some 0); (* always skip visiting the subexpr of NUMERAL *)
add_thms [obind; LET_END_DEF] rw;
(* Do not add _BITMATCH. These will be covered by conceal_bitmatch. *)
add_conv (`_MATCH:A->(A->B->bool)->B`, 2, MATCH_CONV) rw;
Expand Down

0 comments on commit f6321f2

Please sign in to comment.