License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.CaseSplit

Description

Given a pattern clause and a variable n, elaborate the clause and find the type of n.

Make new pattern clauses by replacing n with all the possibly constructors applied to '_', and replacing all other variables with '_' in order to resolve other dependencies.

Finally, merge the generated patterns with the original, by matching. Always take the "more specific" argument when there is a discrepancy, i.e. names over '_', patterns over names, etc.

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 -> Int -> String Source #

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

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

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