)]}'
{
  "commit": "f88263cdc9b79784969d8eee57c1c3c98dc51d96",
  "tree": "0ac93acd3686ef85ad0e0c1c86b220c29d89950e",
  "parents": [
    "8f1c18d9f4d9fd5042bec7710c5f57da0216aa93"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Apr 04 00:21:28 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Apr 04 00:21:28 2026 +0000"
  },
  "message": "fix: handle propositional and decidable instances in sym canonicalizer\n\nThis PR refactors instance canonicalization in the sym canonicalizer to\nproperly handle `Grind.nestedProof` and `Grind.nestedDecidable` markers.\nPreviously, the canonicalizer would report an issue when it failed to\nresynthesize propositional instances that were provided by `grind`\nitself or by the user via `haveI`. Now, resynthesis failure gracefully\nfalls back to the original instance in value positions, while remaining\nstrict inside types. This also removes the separate `cacheInsts` cache\nin favor of the existing type/value caches via `withCaching`.\n\nCo-Authored-By: Claude Opus 4.6 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "ace691a1bd3358b2e5f56b4132d1cf82234bedaa",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Canon.lean",
      "new_id": "629b1252f26fbb96962ad58e5e45e3740c1b1017",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Canon.lean"
    },
    {
      "type": "modify",
      "old_id": "130b7208b28e54bee61c2c1996d8f3b4cc4502f3",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/SymM.lean",
      "new_id": "b217d30a565c50f143cb39123ca0e538b5f4eed7",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/SymM.lean"
    },
    {
      "type": "modify",
      "old_id": "b18ebe259841226a15b472c26569a2c4c3954a36",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_indexmap_trace.lean",
      "new_id": "a192fb7ba59c190cb44db52dafa3dcc59463199f",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_indexmap_trace.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "6568a9134f9242068ce600d9f6c98840e2600602",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_prop_inst.lean"
    }
  ]
}