idris-0.9.17.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Coverage

Synopsis

Documentation

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.

genClauses :: FC -> 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!

upd :: t -> PArg' t -> PArg' t Source

collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)] Source