Commit 2023-07-11 22:57 57cae8c0

View on Github →

feat: port Testing.SlimCheck.Functions (#5768) This diverges fairly considerably from mathlib3 since we changed the SampleableExt API when porting the previous file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Testing/SlimCheck/Functions.lean

added def SlimCheck.InjectiveFunction.List.applyId

added theorem SlimCheck.InjectiveFunction.List.applyId_cons

added theorem SlimCheck.InjectiveFunction.List.applyId_eq_self

added theorem SlimCheck.InjectiveFunction.List.applyId_zip_eq

added def SlimCheck.InjectiveFunction.Perm.slice

added def SlimCheck.InjectiveFunction.apply

added theorem SlimCheck.InjectiveFunction.applyId_injective

added theorem SlimCheck.InjectiveFunction.applyId_mem_iff

added def SlimCheck.InjectiveFunction.sliceSizes

added inductive SlimCheck.InjectiveFunction

added def SlimCheck.TotalFunction.List.toFinmap'

added def SlimCheck.TotalFunction.apply

added def SlimCheck.TotalFunction.applyFinsupp

added def SlimCheck.TotalFunction.comp

added def SlimCheck.TotalFunction.reprAux

added def SlimCheck.TotalFunction.shrink

added def SlimCheck.TotalFunction.zeroDefault

added def SlimCheck.TotalFunction.zeroDefaultSupp

added inductive SlimCheck.TotalFunction

Modified Mathlib/Testing/SlimCheck/Sampleable.lean