Oh huh turns out Nat and ℕ are the same thing??

Changes

3 changed files (+16/-17)

• Main.lean
  • @@ -37,8 +37,7 @@ def merge [Ord α] (xs : List α) (ys : List α) : List α :=
    - - def lsb (i : Nat) : Nat := + def lsb (i : ℕ) : ℕ := if i = 0 then 0 else if i % 2 == 1 then 1 else 2 * lsb (i / 2) termination_by i decreasing_by
• lake-manifest.json
  • @@ -5,7 +5,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "84a77eea345d5b6f36803f8780c09d52c876d51f", + "rev": "96f881c550495e6141562b44bd43a3e0d0c4e8d2", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -15,10 +15,10 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fde3fc21dd68a10791dea22b6f5b53c5a5a5962d", + "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient",
  • @@ -35,57 +35,57 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "856a8cb8908af109aac3ce13e2b4f866f3d75199", + "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2d6d124aedc3023506a67e50bfd5582384d6bd17", + "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.63-pre", + "inputRev": "v0.0.67", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a1b5d59f433c6ec2b318192bd910c257a3c62be8", + "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "56047303fce0d07dcae7e3e91b17eef67d11f6f4", + "rev": "867d9dc77534341321179c9aa40fceda675c50d4", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3613427d66262c4e25e19b40a6a49242e94ba072", + "rev": "3cabaef23886b82ba46f07018f2786d9496477d6", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "1604206fcd0462da9a241beeac0e2df471647435", + "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main",
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.22.0-rc2 + leanprover/lean4:v4.22.0-rc3