Changes

12 changed files (+27/-22)

• ac.lean > Choice.lean
• gcd.lean > Gcd.lean
  • @@ -5,10 +5,14 @@ decreasing_by
    rename_i h exact Nat.mod_lt a h - #eval "test" - def N := 1000 def A := List.range N - #eval (A.map λ x => (A.map λ y => gcd x y).sum).sum + def sum := (A.map λ x => (A.map λ y => gcd x y).sum).sum + + #eval sum + + def main := do + IO.println "test" + IO.println sum
• lambcalc.lean > LambCalc.lean
• lazy.lean > Lazy.lean
• monad.lean > Monad.lean
• native-decide.lean > NativeDecide.lean
• palin.lean > Palin.lean
• sum.lean > Sum.lean
• typedlambcalc.lean > TypedLambCalc.lean
• lake-manifest.json
  • @@ -5,7 +5,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "826aa6f3fab98e8a5dd34dbe2f901127b603039e", + "rev": "84a77eea345d5b6f36803f8780c09d52c876d51f", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -15,17 +15,17 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "304c5e2f490d546134c06bf8919e13b175272084", + "rev": "fde3fc21dd68a10791dea22b6f5b53c5a5a5962d", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -35,57 +35,57 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48", + "rev": "856a8cb8908af109aac3ce13e2b4f866f3d75199", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a", + "rev": "2d6d124aedc3023506a67e50bfd5582384d6bd17", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.59", + "inputRev": "v0.0.63-pre", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "417f5fba2ea46d1117c5a8d795d383062b02688e", + "rev": "a1b5d59f433c6ec2b318192bd910c257a3c62be8", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130", + "rev": "56047303fce0d07dcae7e3e91b17eef67d11f6f4", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1a8afbb6f95c4de139dca63cc7454862cb54099a", + "rev": "3613427d66262c4e25e19b40a6a49242e94ba072", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664", + "rev": "1604206fcd0462da9a241beeac0e2df471647435", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main",
• lakefile.toml
  • @@ -2,13 +2,14 @@ name = "leantest"
    version = "0.1.0" defaultTargets = ["leantest"] - [[lean_lib]] - name = "Leantest" - [[lean_exe]] name = "leantest" root = "Main" + [[lean_exe]] + name = "gcd" + root = "Gcd" + [[require]] name = "mathlib" scope = "leanprover-community"
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.20.0-rc5 + leanprover/lean4:v4.22.0-rc2