Agda.TypeChecking.Coverage

Documentation

data SplitClause

Constructors

SClause

Fields

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]

data SplitError

Constructors

NotADatatype Type

neither data type nor record

IrrelevantDatatype Type

data type, but in irrelevant position

NoRecordConstructor Type

record type, but no constructor

CantSplit QName Telescope Args Args [Term]

GenericSplitError String

Instances

Show SplitError

Error SplitError

type CoverM = ExceptionT SplitError TCM

typeOfVar :: Telescope -> Nat -> Arg Type

checkCoverage :: QName -> TCM ()

Top-level function for checking pattern coverage.

cover :: MonadTCM tcm => [Clause] -> SplitClause -> tcm (Set Nat, [[Arg Pattern]])

Check that the list of clauses covers the given split clause. Returns the missing cases.

isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) => Arg Type -> tcm (QName, [Arg Term], [Arg Term], [QName])

Check that a type is a non-irrelevant datatype or a record with named constructor.

computeNeighbourhood :: Telescope -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]

dtype == d pars ixs

splitClause :: Clause -> Nat -> TCM (Either SplitError Covering)

split
x ps.
 ps, x 
(deBruijn index)

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