Lean: cheri_capreg test fails

[protoben]

The cheri_capreg Lean test fails with the following messages:

error: ././././Out.lean:48:9: application type mismatch
  zeros n
argument
  n
has type
  Nat : Type
but is expected to have type
  Unit : Type
error: ././././Out.lean:47:4: fail to show termination for
  Functions.zeros
with errors
failed to infer structural recursion:
Not considering parameter n of Functions.zeros:
  it is unchanged in the recursive calls
Not considering parameter x_1 of Functions.zeros:
  it is unchanged in the recursive calls
no parameters suitable for structural recursion

well-founded recursion cannot be used, 'Functions.zeros' does not take any (non-fixed) arguments
error: ././././Out.lean:192:23: application type mismatch
  capRegToCapStruct (reg_deref CapRegs[i]!)
argument
  reg_deref CapRegs[i]!
has type
  SailM CapReg : Type
but is expected to have type
  BitVec 257 : Type
error: Lean exited with code 1

[javra]

First error is due to a missing pure annotation in the test file, third one is a consequence of the second one, second one is due to reg_deref not being recognized as effectful for some reason