Agda.TypeChecking.Rules.LHS.Implicit

Documentation

insertImplicitProblem :: Problem -> TCM Problem

Insert implicit patterns in a problem.

expandImplicitPattern :: Type -> NamedArg Pattern -> TCM (NamedArg Pattern)

Eta-expand implicit pattern if of record type.

expandImplicitPattern' :: Type -> NamedArg Pattern -> TCM (Maybe (NamedArg Pattern))

Try to eta-expand implicit pattern. Returns Nothing unless dealing with a record type that has eta-expansion and a constructor c. In this case, it returns Just c _ _ ... _ (record constructor applied to as many implicit patterns as there are fields).

implicitP :: Named name (Pattern' e)

insertImplicitPatterns :: ExpandHidden -> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]

Insert implicit patterns in a list of patterns.

insertImplicitPatternsT :: ExpandHidden -> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]