Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

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)

match' :: Stack -> TCM (Reduced (Blocked Args) Term)

unfoldCorecursion :: Term -> TCM (Blocked Term)