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

Safe Haskell | None
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 [WithHiding Expr]
- matchPatternSynP :: PatternSynDefn -> Pattern' e -> Maybe [WithHiding (Pattern' e)]
- mergePatternSynDefs :: List1 PatternSynDefn -> Maybe PatternSynDefn

# Documentation

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

Match an expression against a pattern synonym.

matchPatternSynP :: PatternSynDefn -> Pattern' e -> Maybe [WithHiding (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).