Fix missing case in `casetac`
This looks like a refactoring snafu
commit01c911e0a0a8c74c5a3cfd8a262d514f1bf936e7
authorBrian Koropoff <bkoropoff@gmail.com>
dateMon 13 Jul 2015, 19:50 (11 years ago)
parentc720cf9
src/Idris/Core/ProofState.hs+1−1
@@ -759,7 +759,7 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
759759 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
760760 let var = P Bound idnm idxt
761761 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
762−induction tm induction ctxt env _ = do fail "Can't do induction here"
762+casetac tm induction ctxt env _ = fail $ "Can't do " ++ (if induction then "induction" else "case analysis") ++ " here"
763763
764764
765765equiv :: Raw -> RunTactic