Compute with infinities and infinitesimals! A calculator using the Levi-Civita field, implemented in Lean 4 as a datatype.
a
lean-inf
public
3 stars
0 forks
0 issues
Commits
List of commits on branch main.Unverified
9ea6e5da7c7d619d7a7d63855adbb4596faf5ce6attempt ordered_float in lean
aalok committed 13 days ago
Unverified
eff5e96f34231ab4401cf43110e9d99c6bf743c4rm dummy file
aalok committed 13 days ago
Unverified
8d06e9b533b22c28a1087da6eb2c9092d5e17ef5fix typeclass inference issue
aalok committed 13 days ago
Unverified
7044f3b9e9ebe88a43959feaea7574a133d92949add some instances
aalok committed 13 days ago
Unverified
3f702622b09434c6bb72b94c38882d7473932d97unignore manifest
aalok committed 13 days ago
Unverified
79deb6511f2a61267494ae2acfb6220e7b5646a7add manifest for reservoir
aalok committed 13 days ago