| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.LHS.Implicit
Synopsis
- implicitP :: ArgInfo -> NamedArg Pattern
- insertImplicitPatterns :: ExpandHidden -> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]
- insertImplicitSizeLtPatterns :: Type -> TCM [NamedArg Pattern]
- insertImplicitPatternsT :: ExpandHidden -> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
Documentation
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.