)]}'
{
  "commit": "404a5b735189ceb52f7468315f322c591495c96f",
  "tree": "fc1dd4d10ee86e83677a1bc62ff8d70ceba88210",
  "parents": [
    "96d15f5d485c333e716b30b22172e95c671bf909"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Mar 19 15:54:29 2026 -0400"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Mar 19 15:54:29 2026 -0400"
  },
  "message": "fix: isRfl must ignore contextDependent; add unit tests\n\nisRfl was using `matches .rfl` which only matched when ALL fields\nhave default values. With the new contextDependent field, .rfl false true\n(cd\u003dtrue) no longer matched, causing Theorems.rewrite to incorrectly\nreturn cd .rfl results instead of continuing to the next theorem.\n\nFix: match `.rfl false _` (done\u003dfalse, ignore cd).\n\nAdd unit tests for mkEqTransResult, andThen, orElse cd propagation.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "443900e635ee693b775ea60e5b29929d17cabfd8",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Simp/Result.lean",
      "new_id": "11b086f059f1aa2ef81002833117e6d14a552dcd",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Simp/Result.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "9a9c9f4ee01467ecec574a282f39e4414ab3c1ed",
      "new_mode": 33188,
      "new_path": "tests/elab/sym_simp_cd_unit.lean"
    }
  ]
}