diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 249d0b0bb6..4918004c6d 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -284,6 +284,9 @@ fun stx => let arg := stx.getArg 1; `(pure $arg) +@[builtinMacro Lean.Parser.Term.«sorry»] def expandSorry : Macro := +fun _ => `(sorryAx _ false) + /- TODO @[builtinTermElab] def elabsubst : TermElab := expandInfixOp infixR " ▸ " 75