Agda-2.2.8: A dependently typed functional programming language and proof assistant




data SplitClause Source




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

data SplitError Source


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 

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

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

split  x ps.   ps, x   (deBruijn index)