Skip to content

Commit

Permalink
chore: update Mathlib for leanprover-community/batteries#329
Browse files Browse the repository at this point in the history
  • Loading branch information
semorrison authored and fgdorais committed Nov 1, 2023
1 parent efc9b44 commit 344616f
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 12 deletions.
4 changes: 0 additions & 4 deletions Mathlib/Data/Bool/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -279,10 +279,6 @@ instance linearOrder : LinearOrder Bool where
min_def := by decide
#align bool.linear_order Bool.linearOrder

@[simp] theorem max_eq_or' : max = or := rfl

@[simp] theorem min_eq_and' : min = and := rfl

#align bool.ff_le Bool.false_le

#align bool.le_tt Bool.le_true
Expand Down
16 changes: 8 additions & 8 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,6 @@
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "a71c160b1934814837d37f377efaf2964e55c433",
"opts": {},
"name": "std",
"inputRev?": "main",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover-community/quote4",
"subDir?": null,
"rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
Expand Down Expand Up @@ -40,5 +32,13 @@
"opts": {},
"name": "proofwidgets",
"inputRev?": "v0.0.21",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "0da0e81a141cd26364f8799fb31ae7866ec43fb7",
"opts": {},
"name": "std",
"inputRev?": "main",
"inherited": false}}],
"name": "mathlib"}

0 comments on commit 344616f

Please sign in to comment.