Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K

Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Rules.LHS.Implicit

Synopsis

value implicitP
value insertImplicitPatterns
value insertImplicitSizeLtPatterns
value insertImplicitPatternsT

PackageAgda-2.8.0.2
Exports4
LanguageHaskell2010
LicenceMIT
SourceImplicit.hs

valueimplicitP :: ArgInfo -> NamedArg Pattern

valueinsertImplicitPatterns

:: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
=> ExpandHidden
-> [NamedArg Pattern]
-> Telescope
-> m [NamedArg Pattern]

Insert implicit patterns in a list of patterns. Even if DontExpandLast, trailing SIZELT patterns are inserted.

valueinsertImplicitSizeLtPatterns :: PureTCM m => Type -> m [NamedArg Pattern]

Insert trailing SizeLt patterns, if any.

valueinsertImplicitPatternsT

:: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
=> ExpandHidden
-> [NamedArg Pattern]
-> Type
-> m [NamedArg Pattern]

Insert implicit patterns in a list of patterns. Even if DontExpandLast, trailing SIZELT patterns are inserted.