Agda.TypeChecking.Rules.Def

Definitions by pattern matching

checkFunDef

checkAlias

checkFunDef'

trailingImplicits

dropNonHidden

splitTrailingImplicits

patchUpTrailingImplicits

insertPatterns

data WithFunctionProblem

checkClause

checkWithFunction

checkWhere

containsAbsurdPattern

actualConstructor