Agda-2.2.10: 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]
data SplitError
= NotADatatype Type
| IrrelevantDatatype Type
| CoinductiveDatatype Type
| NoRecordConstructor Type
| CantSplit QName Telescope Args Args [Term]
| GenericSplitError String
type CoverM = ExceptionT SplitError TCM
typeOfVar :: Telescope -> Nat -> Arg Type
checkCoverage :: QName -> TCM ()
cover :: MonadTCM tcm => [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 :: MonadTCM tcm => Induction -> Telescope -> Permutation -> [Arg Pattern] -> Nat -> tcm (Either SplitError Covering)
split' :: MonadTCM tcm => Induction -> 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
data SplitError Source
Constructors
NotADatatype Typeneither data type nor record
IrrelevantDatatype Typedata type, but in irrelevant position
CoinductiveDatatype Typecoinductive data type
NoRecordConstructor Typerecord type, but no constructor
CantSplit QName Telescope Args Args [Term]
GenericSplitError String
type CoverM = ExceptionT SplitError TCMSource
typeOfVar :: Telescope -> Nat -> Arg 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, 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
splitSource
:: MonadTCM tcm
=> InductionCoinductive constructors are allowed if this argument is CoInductive.
-> Telescope
-> Permutation
-> [Arg Pattern]
-> Nat
-> tcm (Either SplitError Covering)
split'Source
:: MonadTCM tcm
=> InductionCoinductive constructors are allowed if this argument is CoInductive.
-> Telescope
-> Permutation
-> [Arg Pattern]
-> Nat
-> tcm (Either SplitError (Either SplitClause Covering))
Produced by Haddock version 2.6.1