Skip to content

Commit

Permalink
Trigger CI for leanprover/lean4#6123
Browse files Browse the repository at this point in the history
  • Loading branch information
leanprover-community-mathlib4-bot committed Dec 3, 2024
2 parents 04c565b + b07115b commit 1c13781
Show file tree
Hide file tree
Showing 6 changed files with 8 additions and 177 deletions.
2 changes: 2 additions & 0 deletions .github/workflows/docs-release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,8 @@ jobs:
- name: Release Docs
uses: softprops/action-gh-release@v2
with:
prerelease: ${{ contains(github.ref, 'rc') }}
make_latest: ${{ !contains(github.ref, 'rc') }}
files: |
docs/docs-${{ github.ref_name }}.tar.gz
docs/docs-${{ github.ref_name }}.zip
Expand Down
1 change: 0 additions & 1 deletion Batteries.lean
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,6 @@ import Batteries.Tactic.ShowUnused
import Batteries.Tactic.SqueezeScope
import Batteries.Tactic.Trans
import Batteries.Tactic.Unreachable
import Batteries.Tactic.Where
import Batteries.Util.Cache
import Batteries.Util.ExtendedBinder
import Batteries.Util.LibraryNote
Expand Down
90 changes: 0 additions & 90 deletions Batteries/Data/UInt.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,6 @@ import Batteries.Classes.Order
@[ext] theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y
| ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl

@[simp] theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl

@[simp] theorem UInt8.toNat_ofNat (n) :
(no_index (OfNat.ofNat n) : UInt8).toNat = n % UInt8.size := rfl

theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt

@[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat := rfl
Expand All @@ -23,19 +18,6 @@ theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt

@[simp] theorem UInt8.toUInt64_toNat (x : UInt8) : x.toUInt64.toNat = x.toNat := rfl

theorem UInt8.toNat_add (x y : UInt8) : (x + y).toNat = (x.toNat + y.toNat) % UInt8.size := rfl

theorem UInt8.toNat_sub (x y : UInt8) :
(x - y).toNat = (UInt8.size - y.toNat + x.toNat) % UInt8.size := rfl

theorem UInt8.toNat_mul (x y : UInt8) : (x * y).toNat = (x.toNat * y.toNat) % UInt8.size := rfl

theorem UInt8.le_antisymm_iff {x y : UInt8} : x = y ↔ x ≤ y ∧ y ≤ x :=
UInt8.ext_iff.trans Nat.le_antisymm_iff

theorem UInt8.le_antisymm {x y : UInt8} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
UInt8.le_antisymm_iff.2 ⟨h1, h2⟩

instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
(fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt8.le_antisymm

Expand All @@ -44,11 +26,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
@[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y
| ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl

@[simp] theorem UInt16.val_val_eq_toNat (x : UInt16) : x.val.val = x.toNat := rfl

@[simp] theorem UInt16.toNat_ofNat (n) :
(no_index (OfNat.ofNat n) : UInt16).toNat = n % UInt16.size := rfl

theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt

@[simp] theorem UInt16.toUInt8_toNat (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
Expand All @@ -57,19 +34,6 @@ theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt

@[simp] theorem UInt16.toUInt64_toNat (x : UInt16) : x.toUInt64.toNat = x.toNat := rfl

theorem UInt16.toNat_add (x y : UInt16) : (x + y).toNat = (x.toNat + y.toNat) % UInt16.size := rfl

theorem UInt16.toNat_sub (x y : UInt16) :
(x - y).toNat = (UInt16.size - y.toNat + x.toNat) % UInt16.size := rfl

theorem UInt16.toNat_mul (x y : UInt16) : (x * y).toNat = (x.toNat * y.toNat) % UInt16.size := rfl

theorem UInt16.le_antisymm_iff {x y : UInt16} : x = y ↔ x ≤ y ∧ y ≤ x :=
UInt16.ext_iff.trans Nat.le_antisymm_iff

theorem UInt16.le_antisymm {x y : UInt16} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
UInt16.le_antisymm_iff.2 ⟨h1, h2⟩

instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
(fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt16.le_antisymm

Expand All @@ -78,11 +42,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
@[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y
| ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl

@[simp] theorem UInt32.val_val_eq_toNat (x : UInt32) : x.val.val = x.toNat := rfl

@[simp] theorem UInt32.toNat_ofNat (n) :
(no_index (OfNat.ofNat n) : UInt32).toNat = n % UInt32.size := rfl

theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt

@[simp] theorem UInt32.toUInt8_toNat (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
Expand All @@ -91,19 +50,6 @@ theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt

@[simp] theorem UInt32.toUInt64_toNat (x : UInt32) : x.toUInt64.toNat = x.toNat := rfl

theorem UInt32.toNat_add (x y : UInt32) : (x + y).toNat = (x.toNat + y.toNat) % UInt32.size := rfl

theorem UInt32.toNat_sub (x y : UInt32) :
(x - y).toNat = (UInt32.size - y.toNat + x.toNat) % UInt32.size := rfl

theorem UInt32.toNat_mul (x y : UInt32) : (x * y).toNat = (x.toNat * y.toNat) % UInt32.size := rfl

theorem UInt32.le_antisymm_iff {x y : UInt32} : x = y ↔ x ≤ y ∧ y ≤ x :=
UInt32.ext_iff.trans Nat.le_antisymm_iff

theorem UInt32.le_antisymm {x y : UInt32} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
UInt32.le_antisymm_iff.2 ⟨h1, h2⟩

instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
(fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt32.le_antisymm

Expand All @@ -112,11 +58,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
@[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y
| ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl

@[simp] theorem UInt64.val_val_eq_toNat (x : UInt64) : x.val.val = x.toNat := rfl

@[simp] theorem UInt64.toNat_ofNat (n) :
(no_index (OfNat.ofNat n) : UInt64).toNat = n % UInt64.size := rfl

theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt

@[simp] theorem UInt64.toUInt8_toNat (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
Expand All @@ -125,19 +66,6 @@ theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt

@[simp] theorem UInt64.toUInt32_toNat (x : UInt64) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl

theorem UInt64.toNat_add (x y : UInt64) : (x + y).toNat = (x.toNat + y.toNat) % UInt64.size := rfl

theorem UInt64.toNat_sub (x y : UInt64) :
(x - y).toNat = (UInt64.size - y.toNat + x.toNat) % UInt64.size := rfl

theorem UInt64.toNat_mul (x y : UInt64) : (x * y).toNat = (x.toNat * y.toNat) % UInt64.size := rfl

theorem UInt64.le_antisymm_iff {x y : UInt64} : x = y ↔ x ≤ y ∧ y ≤ x :=
UInt64.ext_iff.trans Nat.le_antisymm_iff

theorem UInt64.le_antisymm {x y : UInt64} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
UInt64.le_antisymm_iff.2 ⟨h1, h2⟩

instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
(fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt64.le_antisymm

Expand All @@ -146,11 +74,6 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
@[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y
| ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl

@[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl

@[simp] theorem USize.toNat_ofNat (n) :
(no_index (OfNat.ofNat n) : USize).toNat = n % USize.size := rfl

theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
rw [USize.size]

Expand All @@ -172,18 +95,5 @@ theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by

@[simp] theorem UInt32.toUSize_toNat (x : UInt32) : x.toUSize.toNat = x.toNat := rfl

theorem USize.toNat_add (x y : USize) : (x + y).toNat = (x.toNat + y.toNat) % USize.size := rfl

theorem USize.toNat_sub (x y : USize) :
(x - y).toNat = (USize.size - y.toNat + x.toNat) % USize.size := rfl

theorem USize.toNat_mul (x y : USize) : (x * y).toNat = (x.toNat * y.toNat) % USize.size := rfl

theorem USize.le_antisymm_iff {x y : USize} : x = y ↔ x ≤ y ∧ y ≤ x :=
USize.ext_iff.trans Nat.le_antisymm_iff

theorem USize.le_antisymm {x y : USize} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
USize.le_antisymm_iff.2 ⟨h1, h2⟩

instance : Batteries.LawfulOrd USize := .compareOfLessAndEq
(fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt USize.le_antisymm
83 changes: 0 additions & 83 deletions Batteries/Tactic/Where.lean

This file was deleted.

7 changes: 5 additions & 2 deletions BatteriesTest/where.lean
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
import Batteries.Tactic.Where
-- None of these imports are really necessary, except to create namespace mentioned below.
import Lean.Elab.Term
import Lean.Elab.Command
import Batteries.Data.UnionFind.Basic

-- Return to pristine state
set_option linter.missingDocs false
Expand Down Expand Up @@ -68,6 +71,6 @@ open Array renaming map -> listMap
info: open Lean Lean.Meta
open Lean.Elab hiding TermElabM
open Lean.Elab.Command Batteries
open listMap → Array.map
open Array renaming map → listMap
-/
#guard_msgs in #where
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Or add the following to your `lakefile.toml`:
[[require]]
name = "batteries"
scope = "leanprover-community"
version = "main"
rev = "main"
```

Additionally, please make sure that you're using the version of Lean that the current version of `batteries` expects. The easiest way to do this is to copy the [`lean-toolchain`](./lean-toolchain) file from this repository to your project. Once you've added the dependency declaration, the command `lake update` checks out the current version of `batteries` and writes it the Lake manifest file. Don't run this command again unless you're prepared to potentially also update your Lean compiler version, as it will retrieve the latest version of dependencies and add them to the manifest.
Expand Down

0 comments on commit 1c13781

Please sign in to comment.