Fixes docstring breakage from leanprover#7516.

This PR fixes docstring breakage from #7516.

* fix

* fix again

* chore: bump to nightly-2025-03-15

* fix

* harden script

* chore: bump to nightly-2025-03-16

* Update lean-toolchain for testing leanprover/lean4#7516

* lake update

* fixes for leanprover/lean4#7516

* fixes for leanprover/lean4#7516

* partial test fixes

* fix stacks

* "fix" eqns test

* Remove neg instance, there is one upstream now

* chore: bump to nightly-2025-03-17

* lake update

* lake update

* lint

* Update lean-toolchain for testing leanprover/lean4#7522

* Update lean-toolchain for testing leanprover/lean4#5182

* Bump batteries for leanprover/lean4#5182

* simp works

* Fewer unseal

* Trigger CI for leanprover/lean4#5182

* max heartbeats

* update test

* Update lean-toolchain for testing leanprover/lean4#7519

* Update lean-toolchain for testing leanprover/lean4#7302

* Fix

* fixes

* Trigger CI for leanprover/lean4#5182

* chore: bump to nightly-2025-03-18

* Less rfl abuse

* fix `compile_inductive%` regression

* Trigger CI for leanprover/lean4#5182

* Trigger CI for leanprover/lean4#5182

* Trigger CI for leanprover/lean4#5182

* Adapt

* process deprecations

* Update lean-toolchain for testing leanprover/lean4#7558

* Adapt

* deprecations

* chore: bump to nightly-2025-03-19

* chore: fixes for leanprover/lean4#7519

* Update lean-toolchain for testing leanprover/lean4#7544

* lake update

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* Trigger CI for leanprover/lean4#7544

* .

* cleaning up

* chore: bump to nightly-2025-03-20

* update

* deprecation/note about upstreamed version

* fix

* Update lean-toolchain for testing leanprover/lean4#7614

* chore: bump to nightly-2025-03-21

* Adapt back

* fix test output

* chore: bump to nightly-2025-03-22

* Merge master into nightly-testing

* chore: adaptations for nightly-2025-03-22

* fix

* Merge master into nightly-testing

* protected

* chore: bump to nightly-2025-03-24

* update batteries and aesop

* fixes for count_cons_of_ne

* fix fix to Sym.inhabitedSym' (need `default`, not the `a` that happens to be in context)

* bump heartbeats in MathlibTest/observe

* fix, deprecated

* fix merge

* Update lean-toolchain for testing leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* fixes for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* fixes

* chore: bump to nightly-2025-03-25

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* Trigger CI for leanprover/lean4#7672

* one fix

* fixes

* maxheartbeats

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* cleanups

* .

* chore: bump to nightly-2025-03-26

* update aesop

* Update lean-toolchain for testing leanprover/lean4#7690

* Trigger CI for leanprover/lean4#7690

* Trigger CI for leanprover/lean4#7690

* maxHeartbeats

* max heartbeats

* invalidate cache

* another heartbeats

* bump batteries

* deprecation

* Update lean-toolchain for testing leanprover/lean4#7692

* Delete

* chore: bump to nightly-2025-03-27

* update batteries

* bump batteries

* many more maxHeartbeats

* chore: bump leantar v0.1.15

* invalidate cache

* cache flush, take 2

* feat(Cache): root hash generation counter

* 1-line fix

* chore: bump to nightly-2025-03-28

* update deps

* remove upstreamed

* remove all adaptation notes, hooray

* merge lean-pr-testing-7692

* fixes from Kevin's review

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.21.0-rc1

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.22.0-rc1

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.22.0-rc2

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.22.0-rc3

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.22.0-rc4

…ary` instances (#35)

* chore: bump toolchain to v4.19.0

* chore: add #guard_msgs to noisy test

* chore: add #guard_msgs to noisy test

* chore: bump toolchain to v4.20.0-rc1

* chore: bump toolchain to v4.20.0-rc2

* chore: bump toolchain to v4.20.0

* chore: bump toolchain to v4.21.0-rc1 (#26)

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.21.0-rc1

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

* chore: bump toolchain to v4.21.0-rc2 (#27)

* chore: bump toolchain to v4.21.0-rc3 (#28)

* chore: bump toolchain to v4.21.0

* chore: bump toolchain to v4.22.0-rc1 (#30)

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.22.0-rc1

* chore: bump toolchain to v4.22.0-rc2 (#31)

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.22.0-rc2

* chore: bump toolchain to v4.22.0-rc3 (#32)

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.22.0-rc3

* chore: bump toolchain to v4.22.0-rc4 (#34)

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.22.0-rc4

* Derive Arbitrary instances for algebraic data types

* Only import linter from Batteries in Testable.lean

* Specialize imports (avoid importing Lean directly)

* Remove .DS_Store from .gitignore

* Remove comment from Plausible.lean

* Avoid thunking sub-generators

* Update snapshot tests (sub-generators no longer thunked & are now explicitly parenthesized)

* Remove mention of "simple inductive types"

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

* Replace command elaborator with trace class

* Update snapshot tests to use trace class instead of command elaborator

* Update module docs following Kyle's suggestions

* Remove deprecated command elaborator from nolints.json

* Remove unused function

* Rename ArbitrarySized to ArbitraryFueled following Eric's suggestion

* Remove global constants in Idents file

* Update snapshot tests to use size' + 1 instead of Nat.succ size'

* Rename size function parameter in derived generators to fuel

* Add counterexample property to Tree snapshot test

* Add module docs for Tree snapshot test

* Add counterexample property to Regular Expression snapshot test

* Add counterexample property for STLC snapshot test

* Add counterexample property for structure test

* Fix typo in tests

* Add counterexample property for Binop generator test

* Add counterexample property for Value generator test

* Remove unnecessary equality check for booleans

* Add counterexample property for BitVec generator test

* Emit error message when target type has no non-recursive constructors

* Formatting in Random.lean

* Refactor to use same logic as Deriving Repr (handle parameterized types + mutually inductive types)

* Update snapshot tests

* Add implicit parameters to derived generator for parameterized types

* Update tests based on changes to accomodate parameterized types

* Add docstrings to make linter happy

* Handle mutually recursive types (need to add local let-definitions for Arbitrary instances)

* Add snapshot test for mutually recursive types

* Add counterexample property for mutually inductive type test

* Improve shrinkers for trees

* For parameterized types, ArbitraryFueled instances should have inst-implicit Arbitrary binders

* Add counterexample property for parameterized type test

* Remove Idents file, use Core.mkFreshUserName to produce fresh names instead

* Remove mkLetBind (just create let-bind exprs directly using quotations)

* Remove mkMatch combinators, just create match-exprs using quotations

* Remove TSyntaxCombinators file, combinators are no longer used

* Remove unnecessary if-condition

* Refactor: move logic for setting ctorIsRecursive flag

* Simplify logic for determining if constructors are recursive, remove Utils.lean

* Remove spurious instance loop involving SampleableExt -> Arbitrary -> SampleableExt

* Simplify logic for parenthesizing sub-generators

* Loop fusion when computing sub-generator weights

* Clean up nolints.json

* Add newline

* Replace all instances of LocalContext.getUnusedName w/ Core.mkFreshUserName

* Remove mentions of Enum in README

* Remove Enum mention

* Remove linter & dependency on Batteries

* Remove scripts/nolints.json

* Fix typo in regular expression test docstring

* Moving around definitions so that STLC tests compile

* Remove duplicate Arbitrary file, move around definitions some more

* Remove mentions of outdated command elaborator #derive_arbitrary in README

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.23.0-rc1

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.23.0-rc1

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* chore: bump toolchain to v4.24.0-rc1

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* toolchain

* list deprecations

* chore: bump toolchain to v4.26.0-rc1

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* toolchain

* list deprecations

* bump toolchain

* adaptations for leanprover/lean4#12263

* merge lean-pr-testing-12263

* chore: bump toolchain to v4.29.0-rc1