Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Coverage
Synopsis
data SplitClause = SClause {
scTel :: Telescope
scPerm :: Permutation
scPats :: [Arg Pattern]
scSubst :: [Term]
}
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
= NotADatatype Type
| CantSplit QName Telescope Args Args [Term]
| GenericSplitError String
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
Constructors
SClause
scTel :: Telescopetype of variables in scPats
scPerm :: Permutationhow to get from the variables in the patterns to the telescope
scPats :: [Arg Pattern]
scSubst :: [Term]substitution from scTel to old context
type Covering = [SplitClause]Source
typeOfVar :: Telescope -> Nat -> TypeSource
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
Constructors
NotADatatype Type
CantSplit QName Telescope Args Args [Term]
GenericSplitError String
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
Produced by Haddock version 2.6.0