lean-inf Compute with infinities and infinitesimals! A calculator using the Levi-Civita field, implemented in Lean 4 as a datatype.