| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.LHS.Implicit
Synopsis
- implicitP :: ArgInfo -> NamedArg Pattern
- insertImplicitPatterns :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m) => ExpandHidden -> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
- insertImplicitSizeLtPatterns :: PureTCM m => Type -> m [NamedArg Pattern]
- insertImplicitPatternsT :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m) => ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
Documentation
insertImplicitPatterns :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m) => ExpandHidden -> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern] Source #
Insert implicit patterns in a list of patterns.
Even if DontExpandLast, trailing SIZELT patterns are inserted.
insertImplicitSizeLtPatterns :: PureTCM m => Type -> m [NamedArg Pattern] Source #
Insert trailing SizeLt patterns, if any.
insertImplicitPatternsT :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m) => ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern] Source #
Insert implicit patterns in a list of patterns.
Even if DontExpandLast, trailing SIZELT patterns are inserted.