idris-0.9.16: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Coverage

Documentation

mkPatTm :: PTerm -> Idris Term Source

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

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

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

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

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

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

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

checkTotality :: [Name] -> FC -> Name -> Idris Totality Source

checkDeclTotality :: (FC, Name) -> Idris Totality Source

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

delazy :: TT Name -> TT Name Source

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

data Guardedness Source

Constructors

Toplevel 
Unguarded 
Guarded 

Instances

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

checkSizeChange :: Name -> Idris Totality Source

type MultiPath = [SCGEntry] Source

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

checkMP :: IState -> Int -> MultiPath -> Totality Source

allNothing :: [Maybe a] -> Bool Source

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

noPartial :: [Totality] -> Totality Source

collapse :: [Totality] -> Totality Source

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