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

feat: expand sorry

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-10 14:38:26 -07:00
parent ba4fdce508
commit 22bdab67ff
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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