  We describe a new arithmetic system for the Magma computer algebra system for
working with $p$-adic numbers exactly, in the sense that numbers are
represented lazily to infinite $p$-adic precision. This is the first highly
featured such implementation. This has the benefits of increasing
user-friendliness and speeding up some computations, as well as forcibly
producing provable results. We give theoretical and practical justification for
its design and describe some use cases. The intention is that this article will
be of benefit to anyone wanting to implement similar functionality in other
languages.
