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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Patterns.Abstract

Description

Tools to manipulate patterns in abstract syntax in the TCM (type checking monad).

Synopsis

Documentation

expandLitPattern :: Pattern -> TCM Pattern Source #

Expand literal integer pattern into suc/zero constructor patterns.

expandPatternSynonyms' :: forall e. Pattern' e -> TCM (Pattern' e) Source #

Expand away (deeply) all pattern synonyms in a pattern.