Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Abstract.PatternSynonyms

Description

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

Synopsis

Documentation

matchPatternSyn :: PatternSynDefn -> Expr -> Maybe [Arg Expr] Source #

Match an expression against a pattern synonym.

matchPatternSynP :: PatternSynDefn -> Pattern' e -> Maybe [Arg (Pattern' e)] Source #

Match a pattern against a pattern synonym.

mergePatternSynDefs :: 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).