| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Syntax.Internal.Pattern
- clauseArgs :: Clause -> Args
- clauseElims :: Clause -> Elims
- class FunArity a where
- class LabelPatVars a b i | b -> i where
- labelPatVars :: a -> State [i] b
- unlabelPatVars :: b -> a
- numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b
- unnumberPatVars :: LabelPatVars a b i => b -> a
- dbPatPerm :: [NamedArg DeBruijnPattern] -> Permutation
- clausePerm :: Clause -> Permutation
- patternToElim :: Arg DeBruijnPattern -> Elim
- patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim]
- patternToTerm :: DeBruijnPattern -> Term
Tools for clauses
clauseArgs :: Clause -> Args Source
Translate the clause patterns to terms with free variables bound by the clause telescope.
Precondition: no projection patterns.
clauseElims :: Clause -> Elims Source
Translate the clause patterns to an elimination spine with free variables bound by the clause telescope.
Arity of a function, computed from clauses.
Tools for patterns
class LabelPatVars a b i | b -> i where Source
Label the pattern variables from left to right using one label for each variable pattern and one for each dot pattern.
Methods
labelPatVars :: a -> State [i] b Source
unlabelPatVars :: b -> a Source
Intended, but unpractical due to the absence of type-level lambda, is:
labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern' (i,x)))
Instances
| LabelPatVars a b i => LabelPatVars [a] [b] i Source | |
| LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i Source | |
| LabelPatVars (Pattern' x) (Pattern' (i, x)) i Source | |
| LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i Source |
numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b Source
Augment pattern variables with their de Bruijn index.
unnumberPatVars :: LabelPatVars a b i => b -> a Source
clausePerm :: Clause -> Permutation Source
patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim] Source