Update Lean version

Changes

3 changed files (+11/-10)

• lake-manifest.json
  • @@ -5,7 +5,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a97f34f9002eea29dac71f0b294678d702511e2c", + "rev": "826aa6f3fab98e8a5dd34dbe2f901127b603039e", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -15,7 +15,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8cee626a680fe217814c4bd444b94ceb31efd6b6", + "rev": "304c5e2f490d546134c06bf8919e13b175272084", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -35,7 +35,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c20832d6f0b3186a97ea9361cec0a5b87dd152a3", + "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -45,17 +45,17 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ea953247aac573c9b5adea60bacd3e085f58aca4", + "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.56", + "inputRev": "v0.0.59", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "323e9f0b9bd41161ba116fe3bff86fc464d454f2", + "rev": "417f5fba2ea46d1117c5a8d795d383062b02688e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -65,7 +65,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "aa4c87abed970d9dfad2506000d99d30b02f476b", + "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -75,7 +75,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f523fcb75db2b472cda7d94d6caa5d745b1a0c26", + "rev": "1a8afbb6f95c4de139dca63cc7454862cb54099a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -85,7 +85,7 @@
    "type": "git", "subDir": null, "scope": "leanprover", - "rev": "aff4176e5c41737a0d73be74ad9feb6a889bfa98", + "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main",
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.19.0-rc3 + leanprover/lean4:v4.20.0-rc5
• monad.lean
  • @@ -1,3 +1,4 @@
    + -- Need LawfulMonad to guarentee the monad laws hold def mapM [Monad m] (f : α → m β) : List α → m (List β) | [] => pure [] | x :: xs =>