constructive reals via interval arithmetic

Stream: Is there code for X?

[Daniel Shapero]

Hi all -- I've just come across the book Real Analysis: A Constructive Approach Through Interval Arithmetic by Mark Bridger. I searched the zulip for anything about interval arithmetic and came up empty, but I'm wondering if anyone has tried to formalize this approach using Lean before?