Commit 2020-09-10 13:02 d857def3

View on Github →

feat(slim_check): make shrink recursive (#4038) Make example shrinking recursive to make it faster and more reliable. It now acts more like a binary search and less like a linear search.

Estimated changes

Renamed src/data/lazy_list2.lean to src/data/lazy_list/basic.lean

added theorem lazy_list.append_assoc

added theorem lazy_list.append_bind

added theorem lazy_list.append_nil

added def lazy_list.find

added def lazy_list.mfirst

added def lazy_list.reverse

Modified src/data/pnat/basic.lean

added def pnat.nat_pred

Modified src/tactic/interactive.lean

Modified src/testing/slim_check/sampleable.lean

deleted def slim_check.int.shrink'

deleted def slim_check.int.shrink

added def slim_check.iterate_shrink

deleted def slim_check.lazy_list.lseq

added theorem slim_check.list.one_le_sizeof

deleted def slim_check.list.shrink'

added def slim_check.list.shrink_one

added def slim_check.list.shrink_removes

modified def slim_check.list.shrink_with

added theorem slim_check.list.sizeof_append_lt_left

added theorem slim_check.list.sizeof_cons_lt_left

added theorem slim_check.list.sizeof_cons_lt_right

added theorem slim_check.list.sizeof_drop_lt_sizeof_of_lt_length

modified def slim_check.nat.shrink'

modified def slim_check.nat.shrink

added def slim_check.no_shrink.get

added def slim_check.no_shrink.mk

added def slim_check.no_shrink

added def slim_check.prod.shrink

added def slim_check.rec_shrink

modified def slim_check.sampleable.lift

added def slim_check.shrink_fn

added def slim_check.sizeof_lt

modified def slim_check.sum.shrink

added theorem slim_check.tree.one_le_sizeof

modified def slim_check.tree.shrink_with

Modified src/testing/slim_check/testable.lean

modified def slim_check.minimize

added def slim_check.minimize_aux