Agda.TypeChecking.Patterns.Abstract

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

Documentation

expandLitPattern :: (MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) => Pattern -> m Pattern

Expand literal integer pattern into suc/zero constructor patterns.

expandPatternSynonyms' :: forall e. Pattern' e -> TCM (Pattern' e)

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

class ExpandPatternSynonyms a where

Minimal complete definition

Nothing

Methods

expandPatternSynonyms :: a -> TCM a

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

Instances

ExpandPatternSynonyms (Pattern' e)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e)

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms a => ExpandPatternSynonyms [a]

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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