Safe Haskell | None |
---|
- insertImplicitProblem :: Problem -> TCM Problem
- expandImplicitPattern :: Type -> NamedArg Pattern -> TCM (NamedArg Pattern)
- expandImplicitPattern' :: Type -> NamedArg Pattern -> TCM (Maybe (NamedArg Pattern))
- implicitP :: Named name (Pattern' e)
- insertImplicitPatterns :: ExpandHidden -> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]
- insertImplicitPatternsT :: ExpandHidden -> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
Documentation
insertImplicitProblem :: Problem -> TCM ProblemSource
Insert implicit patterns in a problem.
expandImplicitPattern :: Type -> NamedArg Pattern -> TCM (NamedArg Pattern)Source
Eta-expand implicit pattern if of record type.
expandImplicitPattern' :: Type -> NamedArg Pattern -> TCM (Maybe (NamedArg Pattern))Source
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).
insertImplicitPatterns :: ExpandHidden -> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]Source
Insert implicit patterns in a list of patterns.
insertImplicitPatternsT :: ExpandHidden -> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]Source