| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Coverage.SplitPattern
Synopsis
- type SplitPattern = Pattern' SplitPatVar
- data SplitPatVar = SplitPatVar {}
- fromSplitPattern :: NamedArg SplitPattern -> NamedArg DeBruijnPattern
- fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
- toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
- toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
- applySplitPSubst :: TermSubst a => SplitPSubstitution -> a -> a
- isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool
Documentation
type SplitPattern = Pattern' SplitPatVar Source #
data SplitPatVar Source #
For each variable in the patterns of a split clause, we remember the de Bruijn-index and the literals excluded by previous matches.
Constructors
| SplitPatVar | |
Fields | |
Instances
toSplitPSubst :: PatternSubstitution -> SplitPSubstitution Source #
applySplitPSubst :: TermSubst a => SplitPSubstitution -> a -> a Source #
isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool Source #
A pattern that matches anything (modulo eta).