Agda.TypeChecking.Implicit
implicitArgs
implicitNamedArgs
data ImplicitInsertion
impInsert
insertImplicit