Merge pull request #2437 from bkoropoff/fix-missing-case
Fix missing case in `casetac`
commit042c6a51931a808912ba2ff7d30d15c6f60a1872
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 14 Jul 2015, 21:51 (11 years ago)
parentc720cf901c911e
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