Copyright	License : BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell98

Idris.Coverage

Description

Synopsis

Documentation

genClauses :: FC -> Name -> [([Name], Term)] -> [PTerm] -> Idris [PTerm] Source #

Given a list of LHSs, generate a extra clauses which cover the remaining cases. The ones which haven't been provided are marked absurd so that the checker will make sure they can't happen.

This will only work after the given clauses have been typechecked and the names are fully explicit!

validCoverageCase :: Context -> Err -> Bool Source #

Does this error result rule out a case as valid when coverage checking?

recoverableCoverage :: Context -> Err -> Bool Source #

Check whether an error is recoverable in the sense needed for coverage checking.

mkPatTm :: PTerm -> Idris Term Source #

Generate a pattern from an impossible LHS.

We need this to eliminate the pattern clauses which have been provided explicitly from new clause generation.