- data SplitClause = SClause {}
- type Covering = [SplitClause]
- typeOfVar :: Telescope -> Nat -> Type
- checkCoverage :: QName -> TCM ()
- cover :: MonadTCM tcm => [Clause] -> SplitClause -> tcm (Set Nat, [[Arg Pattern]])
- isDatatype :: MonadTCM tcm => Type -> tcm (Maybe (QName, [Arg Term], [Arg Term], [QName]))
- data SplitError
- type CoverM = ExceptionT SplitError TCM
- 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 :: MonadTCM tcm => Telescope -> Permutation -> [Arg Pattern] -> Nat -> tcm (Either SplitError Covering)
- split' :: MonadTCM tcm => Telescope -> Permutation -> [Arg Pattern] -> Nat -> tcm (Either SplitError (Either SplitClause Covering))
Documentation
data SplitClause Source
type Covering = [SplitClause]Source
checkCoverage :: QName -> TCM ()Source
Top-level function for checking pattern coverage.
cover :: MonadTCM tcm => [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 => Type -> tcm (Maybe (QName, [Arg Term], [Arg Term], [QName]))Source
Check that a type is a datatype
data SplitError Source
type CoverM = ExceptionT SplitError TCMSource
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
split :: MonadTCM tcm => Telescope -> Permutation -> [Arg Pattern] -> Nat -> tcm (Either SplitError Covering)Source
split' :: MonadTCM tcm => Telescope -> Permutation -> [Arg Pattern] -> Nat -> tcm (Either SplitError (Either SplitClause Covering))Source