)]}'
{
  "commit": "a4f0b13376e4a07eccb8d9cd4666bf72f94226eb",
  "tree": "bbb63d0ba35d51de6a1e15af5afd8a3f8c26c8a4",
  "parents": [
    "a2ec8251001440c7dda5f060c51276e369ef08b9"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Nov 05 20:35:43 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Nov 05 20:35:43 2026 +0000"
  },
  "message": "fix: `constructorApp\u0027?` on `Nat` offsets `s + 0`\n\nThis PR fixes the internal error `mkNoConfusion: No manifest constructors` in `contradiction` on hypotheses such as `h : 0 + 0 \u003d 1`.\n\n`constructorApp\u0027?` and `isConstructorApp\u0027?` returned `none` for every offset term `s + 0`, but `s + 0` reduces to `s`, which may be a constructor application. They now fall through to the regular `whnf`-based path in this case.\n\nCloses #16285\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "289824870d48f73ed8238968dc433e354356cc63",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/CtorRecognizer.lean",
      "new_id": "ddf1c5a0345ccc5e9fc454617a11f4948f4d5e09",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/CtorRecognizer.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "a9c2a3f305d61638791134945751c3f0b60e1b9f",
      "new_mode": 33188,
      "new_path": "tests/elab/issue16285.lean"
    }
  ]
}