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

Agda.TypeChecking.Coverage

Synopsis

Documentation

data SplitClause Source

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

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

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

split  x ps.   ps, x   (deBruijn index)