Partial support for mutual inductives in derive - #1056

Closed

Janno wants to merge 22 commits into

LPCIC:masterfrom

Janno:janno/mutind-2

Commits on Jul 22, 2026

derive: add shared mutual inductive helpers
Janno
committed
00cdc72
derive: test mutual inductives for param1
Janno
committed
b5e0737
derive: support mutual inductives in eqType_ast
Janno
committed
ea76575
derive: support mutual inductives in tag
Janno
committed
2af7eca
derive: support mutual inductives in fields
Janno
committed
de6e17c
derive: support mutual inductives in map
Janno
committed
f0459c0
derive: support mutual inductives in isK
Janno
committed
33bf525
derive: support mutual inductives in projK
Janno
committed
da0483e
derive: support mutual inductives in bcongr
Janno
committed
d7d7045
derive: skip lenses for mutual inductives
Janno
committed
a58cce0
derive: test lens_laws on mutual inductives
Janno
committed
2068500
derive: support mutual inductives in param1_congr
Janno
committed
952c75c
derive: support mutual inductives in param1_functor
Janno
committed
5b3fbd1
derive: support mutual inductives in param1_inhab
Janno
committed
818d3c3
derive: support mutual inductives in param1_trivial
Janno
committed
50c7e83
derive: support mutual inductives in induction
Janno
committed
26ca00b
derive: support mutual inductives in param2
Janno
committed
f24f35c
derive: support mutual inductives in eqb
Janno
committed
7a0f334
derive: support mutual inductives in eqbcorrect
Janno
committed
8bf27c1
derive: support mutual inductives in eqbOK
Janno
committed
bba9c80

Commits on Jul 23, 2026

Fix expected bodies of derived map functions on types without parameters
Janno
committed
3302d96
Address review comments
Janno
committed
dfc0eaf