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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Patterns.Abstract

Description

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

Synopsis

- expandLitPattern :: (MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) => Pattern -> m Pattern
- expandPatternSynonyms' :: forall e. Pattern' e -> TCM (Pattern' e)
- class ExpandPatternSynonyms a where
  - expandPatternSynonyms :: a -> TCM a

# Documentation

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

Expand literal integer pattern into suc/zero constructor patterns.

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

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

class ExpandPatternSynonyms a where Source #

Minimal complete definition

Nothing

Methods

expandPatternSynonyms :: a -> TCM a Source #

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

#### Instances

Instances details

ExpandPatternSynonyms (Pattern' e) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e) Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Arg a -> TCM (Arg a) Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a) Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Maybe a -> TCM (Maybe a) Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms [a] Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: [a] -> TCM [a] Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Named n a -> TCM (Named n a) Source #