ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Abstract.PatternSynonyms

Pattern synonym utilities: folding pattern synonym definitions for printing and merging pattern synonym definitions to handle overloaded pattern synonyms.

Synopsis

value matchPatternSyn
value matchPatternSynP
value mergePatternSynDefs

PackageAgda-2.8.0.2
Exports3
LanguageHaskell2010
LicenceMIT
SourcePatternSynonyms.hs

valuematchPatternSyn :: PatternSynDefn -> Expr -> Maybe [WithHiding Expr]

Source#

Match an expression against a pattern synonym.

valuematchPatternSynP

:: PatternSynDefn
-> Pattern' e
-> Maybe [WithHiding (Pattern' e)]

Source#

Match a pattern against a pattern synonym.

valuemergePatternSynDefs :: List1 PatternSynDefn -> Maybe PatternSynDefn

Source#

Merge a list of pattern synonym definitions. Fails unless all definitions have the same shape (i.e. equal up to renaming of variables and constructor names).