Support for mutual inductives - #1053

Closed

Janno wants to merge 27 commits into

LPCIC:masterfrom

Janno:janno/mutind

Commits on Jun 19, 2026

Add derive test cases for mutual inductive types
Janno
committed
4a2b834
WIP mutual inductives
Janno
committed
2e1cb99
Assert the exact shape of the generated mutual inductive types
Janno
committed
ed90599
Add support for mutual inductives to standard derive passes
Janno
committed
4691c8a
Counteract cheating
Janno
committed
60b9a90
More mutual inductive derive
Janno
committed
a653701
Fixes + 3-type mutual inductives
Janno
committed
9edc154
eqb and map now compute
Janno
committed
9781033
Generate compute definitions for some derive passes
Janno
committed
817b447
Add more computation tests
Janno
committed
a6e3c77
Fewer axioms, more constants, more honesty
Janno
committed
6fde326
Support mutual inductives for param1_trivial and param1_functor
Janno
committed
e00c585
Do not use is_recursive to find mutual inductives
Janno
committed
27eca42
Fix eqb confusion with parametric types
Janno
committed
db1c6a7
Make derive post-processing aware of mutual inductives
Janno
committed
7bc447d
Add new primitive to reify mutual inductive block without declaration
Janno
committed
8cc8e45
Extend derive tests for non-recursive mutual inductive types
Janno
committed
b253c41
Support mutual inductives in bcongr, isK, projK
Janno
committed
cf068be
Support mutual inductive types in eqbcorrect
Janno
committed
45f95a7
Fail in unsupported cases.
Janno
committed
5d8ec7c
Record expected terms
Janno
committed
32f5305
FIXME expected defs but proofs are transparent
Janno
committed
2a68178
Back to parameters for proofs
Janno
committed
9eef6c0
Support for type-parametric mutual inductives in param1_functor
Janno
committed
49dc7ad
Add support for mutual inductives in induction, eqbcorrect, eqbOK
Janno
committed
9d18e09
Record expected term, not just the expected type
Janno
committed
5b2753d
Progress towards indexed mutual inductives; missing eq, invert, idx2inv
Janno
committed
7f31d39

Navigation Menu

Uh oh!

Support for mutual inductives - #1053

Support for mutual inductives#1053
Janno wants to merge 27 commits into
LPCIC:masterfrom
Janno:janno/mutind

Commits on Jun 19, 2026

Add derive test cases for mutual inductive types

WIP mutual inductives

Assert the exact shape of the generated mutual inductive types

Add support for mutual inductives to standard derive passes

Counteract cheating

More mutual inductive derive

Fixes + 3-type mutual inductives

eqb and map now compute

Generate compute definitions for some derive passes

Add more computation tests

Fewer axioms, more constants, more honesty

Support mutual inductives for param1_trivial and param1_functor

Do not use is_recursive to find mutual inductives

Fix eqb confusion with parametric types

Make derive post-processing aware of mutual inductives

Add new primitive to reify mutual inductive block without declaration

Extend derive tests for non-recursive mutual inductive types

Support mutual inductives in bcongr, isK, projK

Support mutual inductive types in eqbcorrect

Fail in unsupported cases.

Record expected terms

FIXME expected defs but proofs are transparent

Back to parameters for proofs

Support for type-parametric mutual inductives in param1_functor

Add support for mutual inductives in induction, eqbcorrect, eqbOK

Record expected term, not just the expected type

Progress towards indexed mutual inductives; missing eq, invert, idx2inv