The mutual block we are checking.
The functions are numbered according to their order of appearance in this set.
ModuleAgda-2.8.0.2Haskell2010
Agda.Termination.RecCheck
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.
Synopsis
- type MutualNames
- value recursive
- value anyDefs
- PackageAgda-2.8.0.2
- Exports3
- LanguageHaskell2010
- LicenceMIT
- SourceRecCheck.hs
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.
anysDef names a returns all definitions from names
that are used in a.