| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 :: 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

type Covering = [SplitClause] | Source

typeOfVar :: Telescope -> Nat -> Type | 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

Constructors

NotADatatype Type |
CantSplit QName Telescope Args Args [Term] |
GenericSplitError String |

Instances

Show SplitError
Error SplitError

type CoverM = ExceptionT SplitError TCM | Source

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.4.2