| Safe Haskell | None |
|---|---|
| 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' :: 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' :: 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 :: forall (f :: Type -> Type) b. (Traversable f, ExpandPatternSynonyms b, f b ~ a) => a -> TCM a Source #
Instances
| ExpandPatternSynonyms (Pattern' e) Source # | |
Defined in Agda.TypeChecking.Patterns.Abstract | |
| ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) Source # | |
Defined in Agda.TypeChecking.Patterns.Abstract | |
| ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source # | |
Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a) Source # | |
| ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a) Source # | |
Defined in Agda.TypeChecking.Patterns.Abstract | |
| ExpandPatternSynonyms a => ExpandPatternSynonyms [a] Source # | |
Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: [a] -> TCM [a] Source # | |
| ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) Source # | |
Defined in Agda.TypeChecking.Patterns.Abstract | |