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

data SplitError Source

Constructors

NotADatatype Type

neither data type nor record

IrrelevantDatatype Type

data type, but in irrelevant position

CoinductiveDatatype Type

coinductive data type

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

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

split  x ps.   ps, x   (deBruijn index)

splitSource

Arguments

:: Induction

Coinductive constructors are allowed if this argument is CoInductive.

-> Telescope 
-> Permutation 
-> [Arg Pattern] 
-> Nat 
-> TCM (Either SplitError Covering) 

split'Source

Arguments

:: Induction

Coinductive constructors are allowed if this argument is CoInductive.

-> Telescope 
-> Permutation 
-> [Arg Pattern] 
-> Nat 
-> TCM (Either SplitError (Either SplitClause Covering))