idris-1.3.0: Functional Programming Language with Dependent Types
Idris.Interactive
Description
caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris () Source #
addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris () Source #
addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris () Source #
addMissing :: FilePath -> Bool -> Int -> Name -> Idris () Source #
makeWith :: FilePath -> Bool -> Int -> Name -> Idris () Source #
makeCase :: FilePath -> Bool -> Int -> Name -> Idris () Source #
doProofSearch :: FilePath -> Bool -> Bool -> Int -> Name -> [Name] -> Maybe Int -> Idris () Source #
makeLemma :: FilePath -> Bool -> Int -> Name -> Idris () Source #