Lean: pointer_assign test fails

[protoben]

The pointer_assign Lean test fails with the following message:

error: ././././Out.lean:46:13: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  ?m.538
error: ././././Out.lean:46:21: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  ?m.538
error: ././././Out.lean:53:30: unknown identifier 'AB'
error: ././././Out.lean:58:14: application type mismatch
  writeRegRef PreSail.Reg
argument
  PreSail.Reg
has type
  (r : ?m.1402) → PreSail.RegisterRef ?m.1403 (?m.1403 r) : Type
but is expected to have type
  RegisterRef ?m.1401 : Type
error: ././././Out.lean:58:22: failed to synthesize
  CoeT (PreSail.SequentialState RegisterType trivialChoiceSource) x (BitVec 32)
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
Additional diagnostic information may be available using the `set_option diagnostics true` command.
Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: Lean exited with code 1