| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Termination.RecCheck
Description
Checking for recursion:
- We detect truly (co)recursive definitions by computing the dependency graph and checking for cycles.
- This is inexpensive and let us skip the termination check when there's no (co)recursion
Original contribution by Andrea Vezzosi (sanzhiyan). This implementation by Andreas.
Documentation
recursive :: [QName] -> TCM [[QName]] Source #
Given a list of formally mutually recursive functions, check for actual recursive calls in the bodies of these functions. Returns the actually recursive functions as strongly connected components.
As a side effect, update the clauseRecursive field in the
clauses belonging to the given functions.