feat: port Testing.SlimCheck.Functions (#5768)

This diverges fairly considerably from mathlib3 since we changed the `SampleableExt` API when porting the previous file. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Matthew Ballard <matt@mrb.email>
leanprover-community · Jul 11, 2023 · 57cae8c · 57cae8c
1 parent f61c1f2
commit 57cae8c
Show file tree

Hide file tree

Showing 3 changed files with 548 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3031,6 +3031,7 @@ import Mathlib.Tactic.Variable
 import Mathlib.Tactic.WLOG
 import Mathlib.Tactic.Widget.CommDiag
 import Mathlib.Tactic.Zify
+import Mathlib.Testing.SlimCheck.Functions
 import Mathlib.Testing.SlimCheck.Gen
 import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable