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

chore: undo unnecessary change

Browse source
This commit is contained in:
Wojciech Nawrocki 2022-05-09 21:01:49 +02:00 • committed by Leonardo de Moura
parent fbb20d465b
commit 9296afca12
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/Elab/Deriving/FromToJson.lean
View file

@ -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,*])