Lean: pc_no_wildcard test fails

[protoben]

The pc_no_wildcard Lean test fails with the following message:

Warning: Required literal pc_no_wildcard.sail:14.5-8:
14 |    (0b1, _)          => 2,
   |     ^-^
   |
Sail cannot simplify the above pattern match:
This bitvector pattern literal must be kept, as it is required for Sail to show that the surrounding pattern match is complete.
When translated into prover targets (e.g. Lem, Coq) without native bitvector patterns, they may be unable to verify that the match covers all possible cases.

Type error:
pc_no_wildcard.sail:6.13-39:
6 |register R : (bits(1), option(bits(2))) = (0b0, None())
  |             ^------------------------^
  | Unsupported register type