Expand literal integer pattern into suc/zero constructor patterns.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Patterns.Abstract
Tools to manipulate patterns in abstract syntax in the TCM (type checking monad).
- 1 class
- 2 values
- PackageAgda-2.8.0.2
- Exports3
- LanguageHaskell2010
- LicenceMIT
- SourceAbstract.hs
Expand away (deeply) all pattern synonyms in a pattern.
Methods
expandPatternSynonyms :: a -> TCM a
Instances6ExpandPatternSynonyms
ExpandPatternSynonyms (Pattern' e)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.AbstractExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.AbstractExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.AbstractExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.AbstractExpandPatternSynonyms a => ExpandPatternSynonyms [a]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.AbstractExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Abstract