Engine fixes#4

Merged

triviajon merged 8 commits into

triviajon:mainfrom

DIJamner:engine-fixes

Jun 29, 2026

Commits on Jun 28, 2026

Generate induction principles with induction hypotheses

DIJamner
and
claude
committed
Generate induction principles for parametric inductives

DIJamner
and
claude
committed
Reduce applied fixpoints in cbv; free shared match branches once at GC

DIJamner
and
claude
committed
Guard fixpoint reduction on constructor-headed decreasing argument

DIJamner
and
claude
committed
Support rewrite on a quantified IH and applying a redex-typed eliminator

DIJamner
and
claude
committed
Reduce fixpoints over parametric constructors (match alias + map capacity)

DIJamner
and
claude
committed
Document pre-existing dangling-options use-after-return in bugs/

DIJamner
and
claude
committed
Fix dangling MEngineOptions pointer: runtime owns a copy

DIJamner
and
claude
committed