Changes

4 changed files (+12/-12)

• Gcd.lean
  • @@ -11,7 +11,10 @@ def A := List.range N
    def sum := (A.map λ x => (A.map λ y => gcd x y).sum).sum - #eval sum + def sumParallel := (Task.mapList List.sum <| A.map λ x => (Task.spawn λ () => (A.map λ y => gcd x y).sum)) |>.get + + -- #eval sum + -- #eval sumParallel def main := do IO.println "test"
• Leantest.lean (deleted)
  • @@ -1,3 +0,0 @@
    - -- This module serves as the root of the `Leantest` library. - -- Import modules here that should be built as part of the library. - import Leantest.Basic
• lake-manifest.json
  • @@ -5,7 +5,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "96f881c550495e6141562b44bd43a3e0d0c4e8d2", + "rev": "25ad02e863036591086654a3035fc0b4b5354bd4", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -15,7 +15,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5", + "rev": "c37191eba2da78393070da8c4367689d8c4276e4", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -35,7 +35,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873", + "rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -55,7 +55,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244", + "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -65,7 +65,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "867d9dc77534341321179c9aa40fceda675c50d4", + "rev": "1ef3dac0f872ca6aaa7d02e015427e06dd0b6195", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -75,7 +75,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3cabaef23886b82ba46f07018f2786d9496477d6", + "rev": "bea1ecc5f1e6d9a3ab8e9ed72963cc1060b5805e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -85,7 +85,7 @@
    "type": "git", "subDir": null, "scope": "leanprover", - "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386", + "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main",
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.22.0-rc3 + leanprover/lean4:v4.22.0-rc4