diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 4d6b487a10..117e972895 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1117,23 +1117,20 @@ fun stx expectedType? => withMacroExpansion stx pairs (elabTerm pairs expectedType?) | _ => throwError stx "unexpected parentheses notation" -@[builtinTermElab «listLit»] def elabListLit : TermElab := -fun stx expectedType? => do +@[builtinMacro Lean.Parser.Term.listLit] def expandListLit : Macro := +fun stx => let openBkt := stx.getArg 0; let args := stx.getArg 1; let closeBkt := stx.getArg 2; let consId := mkTermIdFrom openBkt `List.cons; let nilId := mkTermIdFrom closeBkt `List.nil; - let newStx := args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId; - withMacroExpansion stx newStx $ elabTerm newStx expectedType? + pure $ args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId -@[builtinTermElab «arrayLit»] def elabArrayLit : TermElab := -fun stx expectedType? => do +@[builtinMacro Lean.Parser.Term.arrayLit] def expandArrayLit : Macro := +fun stx => match_syntax stx with - | `(#[$args*]) => do - newStx ← `(List.toArray [$args*]); - withMacroExpansion stx newStx (elabTerm newStx expectedType?) - | _ => throwError stx "unexpected array literal syntax" + | `(#[$args*]) => `(List.toArray [$args*]) + | _ => throw $ Macro.Exception.error stx "unexpected array literal syntax" private partial def resolveLocalNameAux (lctx : LocalContext) : Name → List String → Option (Expr × List String) | n, projs =>