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

Agda.TypeChecking.Patterns.Abstract

Description

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

Synopsis

Documentation

expandLitPattern :: (MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) => Pattern -> m 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.