Documentation

mkPatTm :: PTerm -> Idris TermSource

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

fnub :: [PTerm] -> [PTerm]Source

fnub' :: [PTerm] -> [PTerm] -> [PTerm]Source

quickEq :: PTerm -> PTerm -> BoolSource

qelem :: PTerm -> [PTerm] -> BoolSource

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

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

checkPositive :: Name -> (Name, Type) -> Idris ()Source

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

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

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

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

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

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 t] -> BoolSource

collapseNothing :: [(Maybe t1, t)] -> [(Maybe t1, t)]Source

noPartial :: [Totality] -> TotalitySource

collapse :: [Totality] -> TotalitySource

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