Agda.TypeChecking.Patterns.Abstract

Tools to manipulate patterns in abstract syntax in the TCM (type checking monad).

Documentation

expandLitPattern :: NamedArg Pattern -> TCM (NamedArg Pattern)

Expand literal integer pattern into suc/zero constructor patterns.

expandPatternSynonyms' :: Pattern -> TCM Pattern

Expand away (deeply) all pattern synonyms in a pattern.

class ExpandPatternSynonyms a where

Methods

expandPatternSynonyms :: a -> TCM a

expandPatternSynonyms :: (Traversable f, ExpandPatternSynonyms b, f b ~ a) => a -> TCM a

Instances

ExpandPatternSynonyms Pattern

Methods

expandPatternSynonyms :: Pattern -> TCM Pattern

ExpandPatternSynonyms a => ExpandPatternSynonyms [a]

Methods

expandPatternSynonyms :: [a] -> TCM [a]

ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a)

Methods

expandPatternSynonyms :: Maybe a -> TCM (Maybe a)

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a)

Methods

expandPatternSynonyms :: Arg a -> TCM (Arg a)

ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)

Methods

expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a)

ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a)

Methods

expandPatternSynonyms :: Named n a -> TCM (Named n a)