diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 85ced09fc5..768ae6fa4e 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1129,20 +1129,6 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := | some expectedType => mkTacticMVar expectedType stx | none => throwError ("invalid 'by' tactic, expected type has not been provided") -@[builtinMacro Lean.Parser.Term.listLit] def expandListLit : Macro := fun stx => - let openBkt := stx[0] - let args := stx[1] - let closeBkt := stx[2] - let consId := mkIdentFrom openBkt `List.cons - let nilId := mkIdentFrom closeBkt `List.nil - return args.getSepArgs.foldr (init := nilId) fun arg r => - Syntax.mkApp consId #[arg, r] - -@[builtinMacro Lean.Parser.Term.arrayLit] def expandArrayLit : Macro := fun stx => - match_syntax stx with - | `(#[$args*]) => `(List.toArray [$args*]) - | _ => throw $ Macro.Exception.error stx "unexpected array literal syntax" - def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do let lctx ← getLCtx let view := extractMacroScopes n diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 5793157b57..c7273e5b7d 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -88,8 +88,6 @@ def structInstField := ppGroup $ parser! structInstLVal >> " := " >> termParser def typeSpec := parser! " : " >> termParser def optType : Parser := optional typeSpec @[builtinTermParser] def subtype := parser! "{ " >> ident >> optType >> " // " >> termParser >> " }" -@[builtinTermParser] def listLit := parser! "[" >> sepBy termParser ", " true >> "]" -@[builtinTermParser] def arrayLit := parser! "#[" >> sepBy termParser ", " true >> "]" @[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec @[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")" def binderIdent : Parser := ident <|> hole