idris-0.9.15.1: Functional Programming Language with Dependent Types
Idris.Coverage
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
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