Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Internal.Pattern
Documentation
data OneHolePatterns Source
Constructors
OHPats [Arg Pattern] (Arg OneHolePattern) [Arg Pattern]
data OneHolePattern Source
Constructors
Hole
OHCon QName (Maybe (Arg Type)) OneHolePatterns

The type serves the same role as the type argument to ConP.

TODO: If a hole is plugged this type may have to be updated in some way.

plugHole :: Pattern -> OneHolePatterns -> [Arg Pattern]Source
allHoles :: [Arg Pattern] -> [OneHolePatterns]Source
allHolesWithContents :: [Arg Pattern] -> [(Pattern, OneHolePatterns)]Source
Produced by Haddock version 2.6.1