Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-03 18:56 b790b27d

View on Github →

feat(slim_check): sampleable instance for generating functions and injective functions (#3967) This also adds printable_prop to trace why propositions hold or don't hold and sampleable_ext to allow the data structure generated and shrunken by slim_check to have a different type from the type we are looking for.

Estimated changes

modified def uliftable.adapt_up
added inductive slim_check.total_function
added def slim_check.large
added def slim_check.small
modified def slim_check.sum.shrink
modified def slim_check.minimize