)]}'
{
  "commit": "7dcb576acbbc2f522eee5bfcb99744070d446f53",
  "tree": "c4e3ec97c02bcaeb87f19f87763ccc6d2916732e",
  "parents": [
    "43aaae7348770036657845521d0451822df05946"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Jun 18 04:14:05 2025 +0900"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Jun 18 04:14:05 2025 +0900"
  },
  "message": "feat: proof-by-reflection support for converting semiring terms into ring ones\n\nThis PR implements the proof-by-reflection infrastructure for\nembedding semiring terms as ring ones.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "eb28925eb8c1f840adcbd09076ec2d76d3fd9dfc",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Ring.lean",
      "new_id": "de19d9223ae8379cc2f68936cefe6ca780e094f0",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Ring.lean"
    },
    {
      "type": "modify",
      "old_id": "f930c52952f4cc6a7186f4cee54f6f622c9cbb2e",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Ring/Envelope.lean",
      "new_id": "da42c90213d62a09895038e9e26d51d63fcaeefc",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Ring/Envelope.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "1939fc2c5b74940882d70b575a2fab033e994f69",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Ring/OfSemiring.lean"
    }
  ]
}