idris-0.10.2: Functional Programming Language with Dependent Types

Safe Haskell	None
Language	Haskell98

Idris.CaseSplit

Documentation

splitOnLine Source

Arguments

:: Int	line number
-> Name	variable
-> FilePath	name of file
-> Idris (Bool, [[(Name, PTerm)]])

replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String] Source

getClause Source

Arguments

:: Int	line number that the type is declared on
-> Name	Function name
-> Name	User given name
-> FilePath	Source file name
-> Idris String

getProofClause Source

Arguments

:: Int	line number that the type is declared
-> Name	Function name
-> FilePath	Source file name
-> Idris String

mkWith :: String -> Name -> String Source

nameMissing :: [PTerm] -> Idris [PTerm] Source

getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t) Source

nameRoot :: [String] -> [Char] -> String Source