Safe Haskell | None |
---|
- clauseArgs :: Clause -> Args
- clauseElims :: Clause -> Elims
- class FunArity a where
- patternsToElims :: Permutation -> [NamedArg Pattern] -> [Elim]
- data OneHolePatterns = OHPats [NamedArg Pattern] (NamedArg OneHolePattern) [NamedArg Pattern]
- data OneHolePattern
- plugHole :: Pattern -> OneHolePatterns -> [NamedArg Pattern]
- allHoles :: [NamedArg Pattern] -> [OneHolePatterns]
- allHolesWithContents :: [NamedArg Pattern] -> [(Pattern, OneHolePatterns)]
Tools for clauses
clauseArgs :: Clause -> ArgsSource
Translate the clause patterns to terms with free variables bound by the clause telescope.
Precondition: no projection patterns.
clauseElims :: Clause -> ElimsSource
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
patternsToElims :: Permutation -> [NamedArg Pattern] -> [Elim]Source
One hole patterns
data OneHolePatterns Source
A OneholePattern
is a linear pattern context P
such that for
any non-projection pattern p
, inserting p
into the single hole P[p]
,
yields again a non-projection pattern.
data OneHolePattern Source
Hole | |
OHCon ConHead ConPatternInfo OneHolePatterns | The type in TODO: If a hole is plugged this type may have to be updated in some way. |
allHoles :: [NamedArg Pattern] -> [OneHolePatterns]Source
allHoles ps
returns for each pattern variable x
in ps
a
context P
such P[x]
is one of the patterns of ps
.
The Ps
are returned in the left-to-right order of the
pattern variables in ps
.
allHolesWithContents :: [NamedArg Pattern] -> [(Pattern, OneHolePatterns)]Source