)]}'
{
  "commit": "a7498d2ba9596dcefaa50312f5d0fad2a5fa40bb",
  "tree": "fba235324c4ae5808dc84e0765e4484fcdb5aa86",
  "parents": [
    "287d46e1f6a7a6136c7996367a9b203d93797d00"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Jun 07 16:02:14 2024 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Jun 07 16:05:25 2024 -0700"
  },
  "message": "fix: uses `PUnit`, `pure ()` forces implicit universe parameter to be `1`\n\nRemark: we should probably elaborate `def`s like we elaborate theorems\nwhen the resulting type is provided.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "991aba147e5480e5c469aa185a3f2f9c76744d29",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Option/Instances.lean",
      "new_id": "0d1cd9c80583ed77dcbcc6c22f4d677658f53ac3",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Option/Instances.lean"
    }
  ]
}