idris-0.9.15: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Coverage

Documentation

mkPatTm :: PTerm -> Idris TermSource

genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]Source

genAll :: IState -> [PTerm] -> [PTerm]Source

upd :: t -> PArg' t -> PArg' tSource

checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()Source

checkPositive :: [Name] -> (Name, Type) -> Idris TotalitySource

calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris TotalitySource

calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris TotalitySource

checkTotality :: [Name] -> FC -> Name -> Idris TotalitySource

checkDeclTotality :: (FC, Name) -> Idris TotalitySource

buildSCG :: (FC, Name) -> Idris ()Source

delazy :: TT Name -> TT NameSource

delazy' :: Bool -> TT Name -> TT NameSource

data Guardedness Source

Constructors

Toplevel 
Unguarded 
Guarded 

Instances

buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]Source

checkSizeChange :: Name -> Idris TotalitySource

type MultiPath = [SCGEntry]Source

mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]Source

checkMP :: IState -> Int -> MultiPath -> TotalitySource

allNothing :: [Maybe a] -> BoolSource

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

noPartial :: [Totality] -> TotalitySource

collapse :: [Totality] -> TotalitySource

collapse' :: Totality -> [Totality] -> TotalitySource