Grammar fix in FileWorker.lean

pull/153/head
Patrick Stevens 3 years ago committed by GitHub
parent 7ad23dab24
commit 87cbcbc4e0
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

@ -109,7 +109,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
| return () -- not a theorem -> ignore
-- Forbid the theorem we are proving currently
if n = levelParams.statementName then
addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to prove itself!"
let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
match lemmasAndDefs.find? (fun l => l.name == n) with

Loading…
Cancel
Save