From 4e3ddf716ed2ec4c613b1e4ea8506db910cccd6d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 11 May 2022 09:50:52 +0200 Subject: [PATCH] refactor: unnecessary quotation kind --- src/Lean/Server/Rpc/Deriving.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean index 714d9f3d0f..1df65d9294 100644 --- a/src/Lean/Server/Rpc/Deriving.lean +++ b/src/Lean/Server/Rpc/Deriving.lean @@ -204,7 +204,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr let mkBody (tgt : Name) (func : Name) : TermElabM Syntax := do let items ← nms.mapM fun nm => `(← $(mkIdent func) $nm) let tm := Syntax.mkApp (mkIdent <| Name.mkStr tgt ctor.getString!) items - `(Parser.Term.termReturn| return $tm:term) + `(return $tm:term) let encArm ← `(matchF| | $(mkPattern indVal.name):term => $(← mkBody packetNm ``rpcEncode)) let decArm ← `(matchF| | $(mkPattern packetNm):term => $(← mkBody indVal.name ``rpcDecode))