Safe Haskell | None |
---|---|
Language | Haskell98 |
- insertImplicitProblem :: Problem -> TCM Problem
- expandImplicitPattern :: Type -> NamedArg Pattern -> TCM (NamedArg Pattern)
- expandImplicitPattern' :: Type -> NamedArg Pattern -> TCM (Maybe (NamedArg Pattern))
- implicitP :: Named_ Pattern
- insertImplicitPatterns :: ExpandHidden -> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]
- insertImplicitSizeLtPatterns :: Type -> TCM [NamedArg Pattern]
- insertImplicitPatternsT :: ExpandHidden -> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
Documentation
insertImplicitProblem :: Problem -> TCM Problem Source
Insert implicit patterns in a problem.
expandImplicitPattern :: Type -> NamedArg Pattern -> TCM (NamedArg Pattern) Source
Eta-expand implicit pattern if of record type.
insertImplicitPatterns :: ExpandHidden -> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern] Source
Insert implicit patterns in a list of patterns.
Even if DontExpandLast
, trailing SIZELT patterns are inserted.
insertImplicitSizeLtPatterns :: Type -> TCM [NamedArg Pattern] Source
Insert trailing SizeLt patterns, if any.
insertImplicitPatternsT :: ExpandHidden -> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern] Source
Insert implicit patterns in a list of patterns.
Even if DontExpandLast
, trailing SIZELT patterns are inserted.