fix: instantiate mvars of indices before instantiating fvars#4717

Merged

nomeata merged 5 commits intoleanprover:masterfrom arthur-adjedj:3246-2

Aug 16, 2024

+19-2

Commits on Aug 9, 2024

fix: instantiate mvars of indices before instantiating fvars
arthur-adjedj
committed
test: ensure all mvars are synthesized before modifying the inductive headers
arthur-adjedj
committed

Commits on Aug 13, 2024

chore: style issue
arthur-adjedj
committed

Commits on Aug 16, 2024

fix: use replaceFVars instead of manually abstracting and instantiating
arthur-adjedj
committed
chore: document issue leanprover#3242
arthur-adjedj
committed