Safe Haskell | Safe-Infered |
---|
Agda.TypeChecking.CompiledClause.Match
Documentation
matchCompiled :: CompiledClauses -> MaybeReducedArgs -> TCM (Reduced (Blocked Args) Term)
type Stack = [(CompiledClauses, MaybeReducedArgs, Args -> Args)]
match :: CompiledClauses -> MaybeReducedArgs -> (Args -> Args) -> Stack -> TCM (Reduced (Blocked Args) Term)
unfoldCorecursion :: Term -> TCM (Blocked Term)