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