Better error message for qed in expressions
The "qed" tactic is really more of a prover command than a tactic per
se. This patch makes it so that the user is informed of this, rather
than having the system throw an internal error.
Fixes #1790.
commit15ab5d59e22a5017e82a1c870e5416d9c95c6887
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateMon 16 Mar 2015, 21:53 (12 years ago)
parentebac088
src/Idris/ElabTerm.hs+1
@@ -1850,6 +1850,7 @@ runTac autoSolve ist perhapsFC fn tac
18501850 Just fc ->
18511851 do fill $ reflectFC fc
18521852 solve
1853+ runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"
18531854 runT x = fail $ "Not implemented " ++ show x
18541855
18551856 runReflected t = do t' <- reify ist t