)]}'
{
  "commit": "64c736ac2c935b81a76db973db1b4fac7155b009",
  "tree": "794dc7829e20ec2060709497a45867f69b63b044",
  "parents": [
    "f843837bfaf4fb64571ddced9fa4cdfde40c8610"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Sun Nov 09 23:50:11 2025 +0100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Sun Nov 09 23:50:11 2025 +0100"
  },
  "message": "feat: add foldl_flatMap and foldr_flatMap theorems\n\nAdd theorems relating folding over flatMapped collections to nested folds\nfor List, Array, and Vector. These theorems enable simplifying complex fold\noperations by showing that (l.flatMap f).foldl g init equals\nl.foldl (fun acc x \u003d\u003e (f x).foldl g acc) init, and similarly for foldr.\n\n🤖 Generated with [Claude Code](https://claude.com/claude-code)\n\nCo-Authored-By: Claude \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "28002610b5252b3fbb8a28bec9264c0ad6897592",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Array/Lemmas.lean",
      "new_id": "9d1dd1d61af292c884af513b1d28170188d9840c",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Array/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "8431bd52e21472df4aa9697c3a31cbcd42ee478c",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Lemmas.lean",
      "new_id": "3596a67b28a0684fbe14834bc96959cd3e75d301",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "529703c7c8b1a6fc9e15233ea1c43ab357823e30",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Vector/Lemmas.lean",
      "new_id": "c619d4c9a6dbc103f3865e56998835af76f4c27d",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Vector/Lemmas.lean"
    }
  ]
}