23772e9 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs−1

@@ -239,7 +239,6 @@ data Command = Quit

239 | Pattelab PTerm

240 | DebugInfo Name

241 | Search PTerm

242− | CaseSplit Name PTerm

243 | CaseSplitAt Bool Int Name

242 | CaseSplitAt Bool Int Name

244 | AddClauseFrom Bool Int Name

243 | AddClauseFrom Bool Int Name

245 | AddProofClauseFrom Bool Int Name

244 | AddProofClauseFrom Bool Int Name

src/Idris/CaseSplit.hs+1−1

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2

3−module Idris.CaseSplit(split, splitOnLine, replaceSplits,

3+module Idris.CaseSplit(splitOnLine, replaceSplits,

4 getClause, getProofClause,

5 mkWith,

6 getUniq, nameRoot) where

src/Idris/REPL.hs−3

@@ -532,9 +532,6 @@ process h fn (Info n)

532 [c] -> classInfo c

533 _ -> iPrintError "Not a class"

534process h fn (Search t) = iPrintError "Not implemented"

535−process h fn (CaseSplit n t)

536− = do tms <- split n t

537− iputStrLn (showSep "\n" (map show tms))

538-- FIXME: There is far too much repetition in the cases below!

535-- FIXME: There is far too much repetition in the cases below!

539process h fn (CaseSplitAt updatefile l n)

536process h fn (CaseSplitAt updatefile l n)

540 = do src <- runIO $ readFile fn

537 = do src <- runIO $ readFile fn