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

chore: remove old elaborator that is not needed anymore

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-11 10:21:57 -07:00
parent 4ddd4c4657
commit 32eabf2ef1
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -662,9 +662,6 @@ fun stx expectedType? => match_syntax stx with
@[builtinTermElab choice] def elabChoice : TermElab := elabAtom
@[builtinTermElab proj] def elabProj : TermElab := elabAtom
@[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom
/- A raw identiier is not a valid term,
but it is nice to have a handler for them because it allows `macros` to insert them into terms. -/
@[builtinTermElab ident] def elabRawIdent : TermElab := elabAtom
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.app;