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

refactor: unnecessary quotation kind

Browse source
This commit is contained in:
Sebastian Ullrich 2022-05-11 09:50:52 +02:00 • committed by Leonardo de Moura
parent 75cbb5904e
commit 4e3ddf716e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/Rpc/Deriving.lean
View file

@ -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))