idris-1.1.1: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

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)]]) 

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 

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