|
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
|
|
|
|
|
|
|
|
Constructors | NotADatatype Type | neither data type nor record
| IrrelevantDatatype Type | data type, but in irrelevant position
| CoinductiveDatatype Type | coinductive data type
| NoRecordConstructor Type | record type, but no constructor
| CantSplit QName Telescope Args Args [Term] | | GenericSplitError String | |
|
|
|
|
|
|
|
|
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 non-irrelevant datatype or a record with
named constructor. Unless the Induction argument is CoInductive
the data type must be inductive.
|
|
|
dtype == d pars ixs |
|
|
split x ps. ps, x (deBruijn index)
|
|
|
|
|
|
|
|
|
|
Produced by Haddock version 2.6.1 |