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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Patterns.Abstract

Description

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

Synopsis

Documentation

expandLitPattern :: Pattern -> TCM 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 #

Methods

expandPatternSynonyms :: a -> TCM a #

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

Instances
ExpandPatternSynonyms a => ExpandPatternSynonyms [a] # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a) # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms (Pattern' e) # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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