Safe Haskell | Safe-Infered |
---|
- data SplitClause = SClause {}
- type Covering = [SplitClause]
- data SplitError
- type CoverM = ExceptionT SplitError TCM
- typeOfVar :: Telescope -> Nat -> Arg Type
- checkCoverage :: QName -> TCM ()
- cover :: [Clause] -> SplitClause -> TCM (Set Nat, [[Arg Pattern]])
- isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) => Induction -> Arg Type -> tcm (QName, [Arg Term], [Arg Term], [QName])
- computeNeighbourhood :: Telescope -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]
- splitClause :: Clause -> Nat -> TCM (Either SplitError Covering)
- splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
- split :: Induction -> Telescope -> Permutation -> [Arg Pattern] -> Nat -> TCM (Either SplitError Covering)
- split' :: Induction -> Telescope -> Permutation -> [Arg Pattern] -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
Documentation
data SplitClause Source
type Covering = [SplitClause]Source
data SplitError Source
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 |
type CoverM = ExceptionT SplitError TCMSource
checkCoverage :: QName -> TCM ()Source
Top-level function for checking pattern coverage.
cover :: [Clause] -> SplitClause -> TCM (Set Nat, [[Arg Pattern]])Source
Check that the list of clauses covers the given split clause. Returns the missing cases.
isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) => Induction -> Arg Type -> tcm (QName, [Arg Term], [Arg Term], [QName])Source
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.
computeNeighbourhood :: Telescope -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]Source
dtype == d pars ixs
splitClause :: Clause -> Nat -> TCM (Either SplitError Covering)Source
split Δ x ps. Δ ⊢ ps, x ∈ Δ (deBruijn index)
splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))Source
:: Induction | Coinductive constructors are allowed if this argument is
|
-> Telescope | |
-> Permutation | |
-> [Arg Pattern] | |
-> Nat | |
-> TCM (Either SplitError Covering) |
:: Induction | Coinductive constructors are allowed if this argument is
|
-> Telescope | |
-> Permutation | |
-> [Arg Pattern] | |
-> Nat | |
-> TCM (Either SplitError (Either SplitClause Covering)) |