Skip to content

alok/lean-inf

Repository files navigation

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.

About

No description, website, or topics provided.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages