|
Agda.TypeChecking.Coverage |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Constructors | SClause | | scTel :: Telescope | type of variables in scPats
| scPerm :: Permutation | how to get from the variables in the patterns to the telescope
| scPats :: [Arg Pattern] | | scSubst :: [Term] | substitution from scTel to old context
|
|
|
|
|
|
|
|
|
|
Top-level function for checking pattern coverage.
|
|
|
Check that the list of clauses covers the given split clause.
Returns the missing cases.
|
|
|
Check that a type is a datatype
|
|
|
Constructors | | Instances | |
|
|
|
|
|
dtype == d pars ixs |
|
|
split x ps. ps, x (deBruijn index)
|
|
|
|
|
|
|
|
Produced by Haddock version 2.4.2 |