Skip to content

Commit 76a79aa

Browse files
chore: Bump mathlib dependency to 6727686 (#527)
Bump `mathlib` dependency to [6727686](leanprover-community/mathlib4@6727686): ci(olean_report): use `lake env` instead of `lake exec` to invoke cache binary (#38712) (2026-04-29) Previously at: [2d59066](leanprover-community/mathlib4@2d59066): refactor(Data/Matrix): protect `Matrix.mul_smul` (#38570) (2026-04-27) _This PR was last updated on 2026-05-01 by [this workflow run](https://github.com/leanprover/cslib/actions/runs/25231473662). It is an automated bump using [downstream-reports/open-bump-pr](https://github.com/leanprover-community/downstream-reports)_ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
1 parent fd066e6 commit 76a79aa

3 files changed

Lines changed: 6 additions & 4 deletions

File tree

Cslib/Logics/Propositional/NaturalDeduction/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,6 @@ public import Mathlib.Data.Finset.Insert
1111
public import Mathlib.Data.Finset.SDiff
1212
public import Mathlib.Data.Finset.Image
1313

14-
@[expose] public section
15-
1614
/-! # Natural deduction for propositional logic
1715
1816
We define, for minimal logic, deduction trees (a `Type`) and derivability (a `Prop`) relative to a
@@ -61,6 +59,8 @@ in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (S
6159
references welcome!)
6260
-/
6361

62+
@[expose] public section
63+
6464
universe u
6565

6666
namespace Cslib.Logic.PL

lake-manifest.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "2d59066e04cb90e9fa4d1393a8cd1ee8ace8daa7",
8+
"rev": "672768680fb7e4eff7dac7ceca12bc3889fd60fd",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "master",
11+
"inputRev": "672768680fb7e4eff7dac7ceca12bc3889fd60fd",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
1414
{"url": "https://github.com/leanprover-community/plausible",

lakefile.toml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ weak.linter.unicodeLinter = false
1818
[[require]]
1919
name = "mathlib"
2020
scope = "leanprover-community"
21+
rev = "672768680fb7e4eff7dac7ceca12bc3889fd60fd"
2122

2223
[[lean_lib]]
2324
name = "Cslib"
@@ -26,6 +27,7 @@ globs = ["Cslib.*"]
2627
[[lean_lib]]
2728
name = "CslibTests"
2829
globs = ["CslibTests.+"]
30+
moreLeanArgs = ["-Dweak.linter.style.header=false"]
2931

3032
[[lean_exe]]
3133
name = "checkInitImports"

0 commit comments

Comments
 (0)