chore: remove left-over TODO

leanprover · Sep 10, 2024 · e1b25b8 · e1b25b8
1 parent 84463ab
commit e1b25b8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -180,7 +180,7 @@ def mkFromJsonBody (ctx : Context) (e : Expr) : TermElabM Term := do
 def mkFromJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   let auxFunName := ctx.auxFunNames[i]!
   let indval     := ctx.typeInfos[i]!
-  let header     ←  mkFromJsonHeader indval --TODO fix header info
+  let header     ←  mkFromJsonHeader indval
   let binders    := header.binders
   Term.elabBinders binders fun _ => do
   let type ← Term.elabTerm header.targetType none