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

Safe Haskell | Safe-Inferred
Language | Haskell2010

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

- matchPatternSyn :: PatternSynDefn -> Expr -> Maybe [Arg Expr]
- matchPatternSynP :: PatternSynDefn -> Pattern' e -> Maybe [Arg (Pattern' e)]
- mergePatternSynDefs :: List1 PatternSynDefn -> Maybe PatternSynDefn

# 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).