Commit 2024-11-01 06:14 318cb718

View on Github →

refactor: move slim_check to plausible (#18459) This moves Mathlib to the now pulled out (and already slightly improved) version of slim_check at https://github.com/leanprover-community/plausible/. I removed both all instances and logic as well as all tests that are already covered by plausible itself and only left what Mathlib needs for itself.

Estimated changes

deleted inductive SlimCheck.InjectiveFunction
deleted inductive SlimCheck.TotalFunction