chore: fix repo

src/Lean/Elab/BuiltinTerm.lean

@@ -162,21 +162,19 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtinTermElab cdot] def elabBadCDot : TermElab := fun stx _ =>
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
-@[builtinTermElab strLit] def elabStrLit : TermElab := fun stx _ => do
+@[builtinTermElab str] def elabStrLit : TermElab := fun stx _ => do
   match stx.isStrLit? with
   | some val => pure $ mkStrLit val
   | none     => throwIllFormedSyntax
 
-@[builtinTermElab str] def elabStrLit' : TermElab := elabStrLit -- TODO remove staging hack
-
 private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr := do
   let typeMVar ← mkFreshTypeMVar MetavarKind.synthetic
   match expectedType? with
   | some expectedType => discard <| isDefEq expectedType typeMVar
   | _                 => pure ()
   return typeMVar
 
-@[builtinTermElab numLit] def elabNumLit : TermElab := fun stx expectedType? => do
+@[builtinTermElab num] def elabNumLit : TermElab := fun stx expectedType? => do
   let val ← match stx.isNatLit? with
     | some val => pure val
     | none     => throwIllFormedSyntax
@@ -187,14 +185,12 @@ private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr :=
   registerMVarErrorImplicitArgInfo mvar.mvarId! stx r
   return r
 
-@[builtinTermElab num] def elabNumLit' : TermElab := elabNumLit -- TODO remove staging hack
-
 @[builtinTermElab rawNatLit] def elabRawNatLit : TermElab :=  fun stx expectedType? => do
   match stx[1].isNatLit? with
   | some val => return mkRawNatLit val
   | none     => throwIllFormedSyntax
 
-@[builtinTermElab scientificLit]
+@[builtinTermElab scientific]
 def elabScientificLit : TermElab := fun stx expectedType? => do
   match stx.isScientificLit? with
   | none        => throwIllFormedSyntax
@@ -206,23 +202,17 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
     registerMVarErrorImplicitArgInfo mvar.mvarId! stx r
     return r
 
-@[builtinTermElab scientific] def elabScientificLit' : TermElab := elabScientificLit -- TODO remove staging hack
-
-@[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do
+@[builtinTermElab char] def elabCharLit : TermElab := fun stx _ => do
   match stx.isCharLit? with
   | some val => return mkApp (Lean.mkConst ``Char.ofNat) (mkRawNatLit val.toNat)
   | none     => throwIllFormedSyntax
 
-@[builtinTermElab char] def elabCharLit' : TermElab := elabCharLit -- TODO remove staging hack
-
 /- A literal of type `Name`. -/
 @[builtinTermElab quotedName] def elabQuotedName : TermElab := fun stx _ =>
   match stx[0].isNameLit? with
   | some val => pure $ toExpr val
   | none     => throwIllFormedSyntax
 
-@[builtinTermElab name] def elabQuotedName' : TermElab := elabQuotedName -- TODO remove staging hack
-
 /--
 A resolved name literal. Evaluates to the full name of the given constant if
 existent in the current context, or else fails. -/

src/Lean/Level.lean

@@ -446,9 +446,9 @@ protected partial def Result.quote (r : Result) (prec : Nat) : Syntax :=
     if prec > 0 then Unhygienic.run `(level| ( $s )) else s
   match r with
   | Result.leaf n         => Unhygienic.run `(level| $(mkIdent n):ident)
-  | Result.num  k         => Unhygienic.run `(level| $(quote k):numLit)
+  | Result.num  k         => Unhygienic.run `(level| $(quote k):num)
   | Result.offset r 0     => Result.quote r prec
-  | Result.offset r (k+1) => addParen <| Unhygienic.run `(level| $(Result.quote r 65) + $(quote (k+1)):numLit)
+  | Result.offset r (k+1) => addParen <| Unhygienic.run `(level| $(Result.quote r 65) + $(quote (k+1)):num)
   | Result.maxNode rs     => addParen <| Unhygienic.run `(level| max $(rs.toArray.map (Result.quote · max_prec))*)
   | Result.imaxNode rs    => addParen <| Unhygienic.run `(level| imax $(rs.toArray.map (Result.quote · max_prec))*)
 

src/Lean/Parser.lean

@@ -60,10 +60,10 @@ def mkAntiquot.parenthesizer (name : String) (kind : Option SyntaxNodeKind) (ano
 -- The parenthesizer auto-generated these instances correctly, but tagged them with the wrong kind, since the actual kind
 -- (e.g. `ident`) is not equal to the parser name `Lean.Parser.Term.ident`.
 @[builtinParenthesizer ident] def ident.parenthesizer : Parenthesizer := Parser.Term.ident.parenthesizer
-@[builtinParenthesizer numLit] def numLit.parenthesizer : Parenthesizer := Parser.Term.num.parenthesizer
-@[builtinParenthesizer scientificLit] def scientificLit.parenthesizer : Parenthesizer := Parser.Term.scientific.parenthesizer
-@[builtinParenthesizer charLit] def charLit.parenthesizer : Parenthesizer := Parser.Term.char.parenthesizer
-@[builtinParenthesizer strLit] def strLit.parenthesizer : Parenthesizer := Parser.Term.str.parenthesizer
+@[builtinParenthesizer num] def numLit.parenthesizer : Parenthesizer := Parser.Term.num.parenthesizer
+@[builtinParenthesizer scientific] def scientificLit.parenthesizer : Parenthesizer := Parser.Term.scientific.parenthesizer
+@[builtinParenthesizer char] def charLit.parenthesizer : Parenthesizer := Parser.Term.char.parenthesizer
+@[builtinParenthesizer str] def strLit.parenthesizer : Parenthesizer := Parser.Term.str.parenthesizer
 
 open Lean.Parser
 
@@ -91,10 +91,10 @@ def mkAntiquot.formatter (name : String) (kind : Option SyntaxNodeKind) (anonymo
   Parser.mkAntiquot.formatter name kind anonymous
 
 @[builtinFormatter ident] def ident.formatter : Formatter := Parser.Term.ident.formatter
-@[builtinFormatter numLit] def numLit.formatter : Formatter := Parser.Term.num.formatter
-@[builtinFormatter scientificLit] def scientificLit.formatter : Formatter := Parser.Term.scientific.formatter
-@[builtinFormatter charLit] def charLit.formatter : Formatter := Parser.Term.char.formatter
-@[builtinFormatter strLit] def strLit.formatter : Formatter := Parser.Term.str.formatter
+@[builtinFormatter num] def numLit.formatter : Formatter := Parser.Term.num.formatter
+@[builtinFormatter scientific] def scientificLit.formatter : Formatter := Parser.Term.scientific.formatter
+@[builtinFormatter char] def charLit.formatter : Formatter := Parser.Term.char.formatter
+@[builtinFormatter str] def strLit.formatter : Formatter := Parser.Term.str.formatter
 
 open Lean.Parser