@@ -212,6 +212,15 @@ updateMeta brack (c:cs) n new
212212 = c : updateMeta (brack || not (isSpace c)) cs n new
213213updateMeta brack [] n new = ""
214214
215+checkProv line n = isProv' False line n
216+ where
217+ isProv' p cs n | take (length n) cs == n = p
218+ isProv' _ ('?':cs) n = isProv' False cs n
219+ isProv' _ ('{':cs) n = isProv' True cs n
220+ isProv' _ ('}':cs) n = isProv' True cs n
221+ isProv' p (_:cs) n = isProv' p cs n
222+ isProv' _ [] n = False
223+
215224addBracket False new = new
216225addBracket True new@('(':xs) | last xs == ')' = new
217226addBracket True new | any isSpace new = '(' : new ++ ")"
@@ -223,23 +232,37 @@ makeLemma h fn updatefile l n
223232 = do src <- runIO $ readFile fn
224233 let (before, tyline : later) = splitAt (l-1) (lines src)
225234
235+ -- if the name is in braces, rather than preceded by a ?, treat it
236+ -- as a lemma in a provisional definition
237+
238+ let isProv = checkProv tyline (show n)
239+
226240 ctxt <- getContext
227241 mty <- case lookupTy n ctxt of
228242 [t] -> return t
229243 [] -> ierror (NoSuchVariable n)
230244 ns -> ierror (CantResolveAlts (map show ns))
231−
232245 i <- getIState
233− let skip = guessImps (tt_ctxt i) mty
234246
235− let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
236− let lem_app = show n ++ appArgs skip mty
247+ if (not isProv) then do
248+ let skip = guessImps (tt_ctxt i) mty
237249
238− if updatefile then
239− do let fb = fn ++ "~"
240− runIO $ writeFile fb (addLem before tyline lem lem_app later)
241− runIO $ copyFile fb fn
242− else ihPrintResult h $ lem ++ "\n" ++ lem_app
250+ let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
251+ let lem_app = show n ++ appArgs skip mty
252+
253+ if updatefile then
254+ do let fb = fn ++ "~"
255+ runIO $ writeFile fb (addLem before tyline lem lem_app later)
256+ runIO $ copyFile fb fn
257+ else ihPrintResult h $ lem ++ "\n" ++ lem_app
258+ else do -- provisional definition
259+ let lem_app = show n ++ appArgs [] mty ++
260+ " = ?" ++ show n ++ "_rhs"
261+ if updatefile then
262+ do let fb = fn ++ "~"
263+ runIO $ writeFile fb (addProv before tyline lem_app later)
264+ runIO $ copyFile fb fn
265+ else ihPrintResult h $ lem_app
243266
244267 where getIndent s = length (takeWhile isSpace s)
245268
@@ -279,11 +302,21 @@ makeLemma h fn updatefile l n
279302
280303 addLem before tyline lem lem_app later
281304 = let (bef_end, blankline : bef_start)
282− = span (not . blank) (reverse before)
305+ = case span (not . blank) (reverse before) of
306+ (bef, []) -> (bef, "" : [])
307+ x -> x
283308 mvline = updateMeta False tyline (show n) lem_app in
284309 unlines $ reverse bef_start ++
285310 [blankline, lem, blankline] ++
286311 reverse bef_end ++ mvline : later
287312
288−
313+ addProv before tyline lem_app later
314+ = let (later_bef, blankline : later_end)
315+ = case span (not . blank) later of
316+ (bef, []) -> (bef, "" : [])
317+ x -> x in
318+ unlines $ before ++ tyline :
319+ (later_bef ++ [blankline, lem_app, blankline] ++
320+ later_end)
321+
289322