Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rules.LHS.Implicit

Synopsis

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.