Chore: Update Chamelean with the updated handler for deriving Arbitrary instances#35
Merged
ngernest merged 83 commits intometaprogrammingfrom Aug 12, 2025
Merged
Chore: Update Chamelean with the updated handler for deriving Arbitrary instances#35ngernest merged 83 commits intometaprogrammingfrom
Arbitrary instances#35ngernest merged 83 commits intometaprogrammingfrom
Conversation
chore: bump toolchain to v4.19.0
chore: bump toolchain to v4.20.0-rc1
chore: bump toolchain to v4.20.0-rc2
chore: bump toolchain to v4.20.0
* 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
* 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
…licitly parenthesized)
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
…mplicit Arbitrary binders
WIP: Handle parameterized + mutually recursive types when deriving `Arbitrary` instances
Arbitrary from the Plausible PRArbitrary instances
Arbitrary instancesArbitrary instances
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR propagates the changes to the handler for deriving
Arbitraryinstances from leanprover-community#35 to Chamelean.For documentation purposes, we summarize the changes to the handler here:
Arbitraryinstances for supports parameterized types / mutually recursive types. See ParameterizedTypeTest.lean and MutuallyRecursiveTypeTest.lean.Arbitraryderiving handler has been re-implemented following the idioms for the deriving Repr / BEq handlersderiving Arbitrarysnapshot test now comes with an example of how the derived generator produces a counter-example that refutes some (erroneous) property#derive_generator, we have a trace class trace.plausible.deriving.arbitrary that prints the code for the derived generator if the user enables the option.Note: Some imports & definitions (e.g. for the STLC snapshot tests) have been moved around so that everything compiles.