From 9296afca122966424168910ae8fb0bec98abb741 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 9 May 2022 21:01:49 +0200 Subject: [PATCH] chore: undo unnecessary change --- src/Lean/Elab/Deriving/FromToJson.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index 3805b8c3d5..2147e50e7f 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -28,7 +28,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false) let fields : Array Syntax ← fields.mapM fun field => do let (isOptField, nm) := mkJsonField field - if isOptField then `($(mkIdent ``Json.opt) $nm (some $(mkIdent <| header.targetNames[0] ++ field))) + if isOptField then `(opt $nm (some $(mkIdent <| header.targetNames[0] ++ field))) else `([($nm, toJson $(mkIdent <| header.targetNames[0] ++ field))]) let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:explicitBinder* := mkObj <| List.join [$fields,*])