Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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

implicitP :: ArgInfo -> NamedArg Pattern Source #

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.