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

Agda.Syntax.Internal.Pattern

Documentation

data OneHolePatterns Source

Constructors

OHPats [Arg Pattern] (Arg OneHolePattern) [Arg Pattern]

Instances

Show OneHolePatterns

data OneHolePattern Source

Constructors

Hole
OHCon QName OneHolePatterns

Instances

Show OneHolePattern

plugHole :: Pattern -> OneHolePatterns -> [Arg Pattern]Source

allHoles :: [Arg Pattern] -> [OneHolePatterns]Source

allHolesWithContents :: [Arg Pattern] -> [(Pattern, OneHolePatterns)]Source