Update Lean to v4.27.0

Changes

4 changed files (+5/-5)

• Tests/SQLite.lean
  • @@ -9,7 +9,7 @@ instance (b : Bool) : Testable b :=
    if h : b = true then .isTrue h else - .isFalse h s!"Expected true but got false" + .isFalse h (msg := s!"Expected true but got false") structure TestContext where conn : Connection
• lake-manifest.json
  • @@ -5,10 +5,10 @@ [{"url": "https://github.com/argumentcomputer/lspec/",
    "type": "git", "subDir": null, "scope": "", - "rev": "b05e6b83798bce0887eb5001cb10fdcbe675dde3", + "rev": "8e6ddb17c2b7e2bbb63585aa4225c5b0701b8ad2", "name": "LSpec", "manifestFile": "lake-manifest.json", - "inputRev": "b05e6b83798bce0887eb5001cb10fdcbe675dde3", + "inputRev": "main", "inherited": false, "configFile": "lakefile.toml"}], "name": "sqlite",
• lakefile.lean
  • @@ -41,4 +41,4 @@ moreLinkObjs := #[libsqlite]
    moreLinkArgs := if !Platform.isWindows then #["-Wl,--unresolved-symbols=ignore-all"] else #[] -- Same as above require LSpec from git - "https://github.com/argumentcomputer/lspec/" @ "b05e6b83798bce0887eb5001cb10fdcbe675dde3" + "https://github.com/argumentcomputer/lspec/" @ "main"
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.25.1 + leanprover/lean4:v4.27.0