Skip to content

feat(DeriveArbitrary): Support structure-parameterized types#80

Open
mwhicks1 wants to merge 1 commit into
leanprover-community:mainfrom
mwhicks1:derive-arbitrary-parameterized
Open

feat(DeriveArbitrary): Support structure-parameterized types#80
mwhicks1 wants to merge 1 commit into
leanprover-community:mainfrom
mwhicks1:derive-arbitrary-parameterized

Conversation

@mwhicks1
Copy link
Copy Markdown
Contributor

Extend the Arbitrary deriving handler to support inductive types parameterized by structures. For structure parameters, recursively expand Type-valued fields into per-field inst-implicit binders (e.g., [Arbitrary T.Meta] or [Arbitrary T.base.IDMeta] for nested structures).

Add mkArbitraryInstBinders which replaces mkInstImplicitBinders in mkHeaderWithOnlyImplicitBinders and mkArbitraryFueledInstanceCmds. For each parameter:

  • If [Arbitrary param] is type-correct, emit it (existing behavior)
  • Otherwise, if the param's type is a structure, recursively expand its fields, emitting [Arbitrary proj] for each Type-valued leaf
  • Reject structures with non-Type, non-structure fields (effectively indexed types) with a clear error message

Add StructureParameterTest.lean covering:

  • Simple structure parameters
  • Mixed normal type + structure parameters
  • Nested structure parameters (structure containing structure)
  • Rejection of structures with non-Type fields

Extend the Arbitrary deriving handler to support inductive types
parameterized by structures. For structure parameters, recursively
expand Type-valued fields into per-field inst-implicit binders
(e.g., [Arbitrary T.Meta] or [Arbitrary T.base.IDMeta] for nested
structures).

Add mkArbitraryInstBinders which replaces mkInstImplicitBinders in
mkHeaderWithOnlyImplicitBinders and mkArbitraryFueledInstanceCmds.
For each parameter:
- If [Arbitrary param] is type-correct, emit it (existing behavior)
- Otherwise, if the param's type is a structure, recursively expand
  its fields, emitting [Arbitrary proj] for each Type-valued leaf
- Reject structures with non-Type, non-structure fields (effectively
  indexed types) with a clear error message

Add StructureParameterTest.lean covering:
- Simple structure parameters
- Mixed normal type + structure parameters
- Nested structure parameters (structure containing structure)
- Rejection of structures with non-Type fields
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant