| Safe Haskell | None |
|---|
Agda.Termination.Inlining
Description
This module defines an inlining transformation on clauses that's run before termination checking. The purpose is to improve termination checking of with clauses (issue 59). The transformation inlines generated with-functions expanding the clauses of the parent function in such a way that termination checking the expanded clauses guarantees termination of the original function, while allowing more terminating functions to be accepted. It does in no way pretend to preserve the semantics of the original function.
Roughly, the source program
f ps with as
{f ps