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

Safe Haskell | None

Agda.Syntax.Internal.Pattern

# Documentation

data OneHolePatterns

Constructors

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

Instances

Show OneHolePatterns |

data OneHolePattern

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.

Instances

Show OneHolePattern |

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

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

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