Agda-2.2.8: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.CompiledClause.Match
matchCompiled :: CompiledClauses -> Args -> TCM (Reduced (Blocked Args) Term)Source
type Stack = [(CompiledClauses, Args, Args -> Args)]Source
match :: CompiledClauses -> Args -> (Args -> Args) -> Stack -> TCM (Reduced (Blocked Args) Term)Source
match' :: Stack -> TCM (Reduced (Blocked Args) Term)Source