Getting a dictionary of aligns in a json file

Stream: mathlib4

[Eric Wieser]

How do I fix the errors here?

import Mathlib.Mathport.Rename
-- import Mathlib -- uncomment to slow things down

open Lean Lean.Elab IO.FS

#eval show MetaM _ from do
  let e ← getEnv
  let l := (Mathlib.Prelude.Rename.getRenameMap e).toLean4.toList
  let j := toJson l
  withFile "translate.json" Mode.write fun h => do h.write s!"{j}"

[Alex J. Best]

use putStr instead of write?

[Eric Wieser]

I ended up just hacking fix-comments.py locally to do what I needed: #6026