Agda.Syntax.Internal.Pattern
Documentation
data OneHolePatterns
Instances
data OneHolePattern
Constructors
Hole | |
OHCon QName (Maybe (Arg Type)) OneHolePatterns | The type serves the same role as the type
argument to TODO: If a hole is plugged this type may have to be updated in some way. |
Instances
plugHole :: Pattern -> OneHolePatterns -> [Arg Pattern]
allHoles :: [Arg Pattern] -> [OneHolePatterns]
allHolesWithContents :: [Arg Pattern] -> [(Pattern, OneHolePatterns)]