36b477e · 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

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

536 [c] -> classInfo c

537 _ -> iPrintError "Not a class"

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

539−process h fn (CaseSplit n t)

540− = do tms <- split n t

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

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

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

543process h fn (CaseSplitAt updatefile l n)

540process h fn (CaseSplitAt updatefile l n)

544 = do src <- runIO $ readFile fn

541 = do src <- runIO $ readFile fn