max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: generate warning when sorry is used

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-13 06:32:39 -08:00
parent 351285a2e8
commit 3ca0aef098
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/BuiltinNotation.lean
View file

@ -189,8 +189,10 @@ private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
else
`(dbgTrace (toString $arg) fun _ => $body)
@[builtinMacro Lean.Parser.Term.«sorry»] def expandSorry : Macro := fun _ =>
`(sorryAx _ false)
@[builtinTermElab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
logWarning "declaration uses 'sorry'"
let stxNew ← `(sorryAx _ false)
withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
@[builtinTermElab emptyC] def expandEmptyC : TermElab := fun stx expectedType? => do
let stxNew ← `(EmptyCollection.emptyCollection)