Skip to content

Commit 2cd17bb

Browse files
leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
committed
Update lean-toolchain for leanprover/lean4#10785 
2 parents d96d9a2 + 2ff6418 commit 2cd17bb

File tree

174 files changed

+1295
-601
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

174 files changed

+1295
-601
lines changed

‎Batteries.lean‎

Lines changed: 115 additions & 113 deletions
Original file line numberDiff line numberDiff line change
@@ -1,113 +1,115 @@
1-
import Batteries.Classes.Cast
2-
import Batteries.Classes.Deprecated
3-
import Batteries.Classes.Order
4-
import Batteries.Classes.RatCast
5-
import Batteries.Classes.SatisfiesM
6-
import Batteries.CodeAction
7-
import Batteries.CodeAction.Attr
8-
import Batteries.CodeAction.Basic
9-
import Batteries.CodeAction.Deprecated
10-
import Batteries.CodeAction.Match
11-
import Batteries.CodeAction.Misc
12-
import Batteries.Control.AlternativeMonad
13-
import Batteries.Control.ForInStep
14-
import Batteries.Control.ForInStep.Basic
15-
import Batteries.Control.ForInStep.Lemmas
16-
import Batteries.Control.LawfulMonadState
17-
import Batteries.Control.Lemmas
18-
import Batteries.Control.Monad
19-
import Batteries.Control.Nondet.Basic
20-
import Batteries.Control.OptionT
21-
import Batteries.Data.Array
22-
import Batteries.Data.AssocList
23-
import Batteries.Data.BinaryHeap
24-
import Batteries.Data.BinomialHeap
25-
import Batteries.Data.BitVec
26-
import Batteries.Data.ByteArray
27-
import Batteries.Data.ByteSlice
28-
import Batteries.Data.Char
29-
import Batteries.Data.DList
30-
import Batteries.Data.Fin
31-
import Batteries.Data.FloatArray
32-
import Batteries.Data.HashMap
33-
import Batteries.Data.Int
34-
import Batteries.Data.List
35-
import Batteries.Data.MLList
36-
import Batteries.Data.NameSet
37-
import Batteries.Data.Nat
38-
import Batteries.Data.PairingHeap
39-
import Batteries.Data.RBMap
40-
import Batteries.Data.Random
41-
import Batteries.Data.Range
42-
import Batteries.Data.Rat
43-
import Batteries.Data.Stream
44-
import Batteries.Data.String
45-
import Batteries.Data.UInt
46-
import Batteries.Data.UnionFind
47-
import Batteries.Data.Vector
48-
import Batteries.Lean.AttributeExtra
49-
import Batteries.Lean.EStateM
50-
import Batteries.Lean.Except
51-
import Batteries.Lean.Expr
52-
import Batteries.Lean.Float
53-
import Batteries.Lean.HashMap
54-
import Batteries.Lean.HashSet
55-
import Batteries.Lean.IO.Process
56-
import Batteries.Lean.Json
57-
import Batteries.Lean.LawfulMonad
58-
import Batteries.Lean.LawfulMonadLift
59-
import Batteries.Lean.Meta.Basic
60-
import Batteries.Lean.Meta.DiscrTree
61-
import Batteries.Lean.Meta.Expr
62-
import Batteries.Lean.Meta.Inaccessible
63-
import Batteries.Lean.Meta.InstantiateMVars
64-
import Batteries.Lean.Meta.SavedState
65-
import Batteries.Lean.Meta.Simp
66-
import Batteries.Lean.Meta.UnusedNames
67-
import Batteries.Lean.MonadBacktrack
68-
import Batteries.Lean.NameMapAttribute
69-
import Batteries.Lean.PersistentHashMap
70-
import Batteries.Lean.PersistentHashSet
71-
import Batteries.Lean.Position
72-
import Batteries.Lean.SatisfiesM
73-
import Batteries.Lean.Syntax
74-
import Batteries.Lean.System.IO
75-
import Batteries.Lean.TagAttribute
76-
import Batteries.Lean.Util.EnvSearch
77-
import Batteries.Linter
78-
import Batteries.Linter.UnnecessarySeqFocus
79-
import Batteries.Linter.UnreachableTactic
80-
import Batteries.Logic
81-
import Batteries.Tactic.Alias
82-
import Batteries.Tactic.Basic
83-
import Batteries.Tactic.Case
84-
import Batteries.Tactic.Congr
85-
import Batteries.Tactic.Exact
86-
import Batteries.Tactic.HelpCmd
87-
import Batteries.Tactic.Init
88-
import Batteries.Tactic.Instances
89-
import Batteries.Tactic.Lemma
90-
import Batteries.Tactic.Lint
91-
import Batteries.Tactic.Lint.Basic
92-
import Batteries.Tactic.Lint.Frontend
93-
import Batteries.Tactic.Lint.Misc
94-
import Batteries.Tactic.Lint.Simp
95-
import Batteries.Tactic.Lint.TypeClass
96-
import Batteries.Tactic.NoMatch
97-
import Batteries.Tactic.OpenPrivate
98-
import Batteries.Tactic.PermuteGoals
99-
import Batteries.Tactic.PrintDependents
100-
import Batteries.Tactic.PrintOpaques
101-
import Batteries.Tactic.PrintPrefix
102-
import Batteries.Tactic.SeqFocus
103-
import Batteries.Tactic.ShowUnused
104-
import Batteries.Tactic.SqueezeScope
105-
import Batteries.Tactic.Trans
106-
import Batteries.Tactic.Unreachable
107-
import Batteries.Util.Cache
108-
import Batteries.Util.ExtendedBinder
109-
import Batteries.Util.LibraryNote
110-
import Batteries.Util.Panic
111-
import Batteries.Util.Pickle
112-
import Batteries.Util.ProofWanted
113-
import Batteries.WF
1+
module
2+
3+
public import Batteries.Classes.Cast
4+
public import Batteries.Classes.Deprecated
5+
public import Batteries.Classes.Order
6+
public import Batteries.Classes.RatCast
7+
public import Batteries.Classes.SatisfiesM
8+
public import Batteries.CodeAction
9+
public import Batteries.CodeAction.Attr
10+
public import Batteries.CodeAction.Basic
11+
public import Batteries.CodeAction.Deprecated
12+
public import Batteries.CodeAction.Match
13+
public import Batteries.CodeAction.Misc
14+
public import Batteries.Control.AlternativeMonad
15+
public import Batteries.Control.ForInStep
16+
public import Batteries.Control.ForInStep.Basic
17+
public import Batteries.Control.ForInStep.Lemmas
18+
public import Batteries.Control.LawfulMonadState
19+
public import Batteries.Control.Lemmas
20+
public import Batteries.Control.Monad
21+
public import Batteries.Control.Nondet.Basic
22+
public import Batteries.Control.OptionT
23+
public import Batteries.Data.Array
24+
public import Batteries.Data.AssocList
25+
public import Batteries.Data.BinaryHeap
26+
public import Batteries.Data.BinomialHeap
27+
public import Batteries.Data.BitVec
28+
public import Batteries.Data.ByteArray
29+
public import Batteries.Data.ByteSlice
30+
public import Batteries.Data.Char
31+
public import Batteries.Data.DList
32+
public import Batteries.Data.Fin
33+
public import Batteries.Data.FloatArray
34+
public import Batteries.Data.HashMap
35+
public import Batteries.Data.Int
36+
public import Batteries.Data.List
37+
public import Batteries.Data.MLList
38+
public import Batteries.Data.NameSet
39+
public import Batteries.Data.Nat
40+
public import Batteries.Data.PairingHeap
41+
public import Batteries.Data.RBMap
42+
public import Batteries.Data.Random
43+
public import Batteries.Data.Range
44+
public import Batteries.Data.Rat
45+
public import Batteries.Data.Stream
46+
public import Batteries.Data.String
47+
public import Batteries.Data.UInt
48+
public import Batteries.Data.UnionFind
49+
public import Batteries.Data.Vector
50+
public import Batteries.Lean.AttributeExtra
51+
public import Batteries.Lean.EStateM
52+
public import Batteries.Lean.Except
53+
public import Batteries.Lean.Expr
54+
public import Batteries.Lean.Float
55+
public import Batteries.Lean.HashMap
56+
public import Batteries.Lean.HashSet
57+
public import Batteries.Lean.IO.Process
58+
public import Batteries.Lean.Json
59+
public import Batteries.Lean.LawfulMonad
60+
public import Batteries.Lean.LawfulMonadLift
61+
public import Batteries.Lean.Meta.Basic
62+
public import Batteries.Lean.Meta.DiscrTree
63+
public import Batteries.Lean.Meta.Expr
64+
public import Batteries.Lean.Meta.Inaccessible
65+
public import Batteries.Lean.Meta.InstantiateMVars
66+
public import Batteries.Lean.Meta.SavedState
67+
public import Batteries.Lean.Meta.Simp
68+
public import Batteries.Lean.Meta.UnusedNames
69+
public import Batteries.Lean.MonadBacktrack
70+
public import Batteries.Lean.NameMapAttribute
71+
public import Batteries.Lean.PersistentHashMap
72+
public import Batteries.Lean.PersistentHashSet
73+
public import Batteries.Lean.Position
74+
public import Batteries.Lean.SatisfiesM
75+
public import Batteries.Lean.Syntax
76+
public import Batteries.Lean.System.IO
77+
public import Batteries.Lean.TagAttribute
78+
public import Batteries.Lean.Util.EnvSearch
79+
public import Batteries.Linter
80+
public import Batteries.Linter.UnnecessarySeqFocus
81+
public import Batteries.Linter.UnreachableTactic
82+
public import Batteries.Logic
83+
public import Batteries.Tactic.Alias
84+
public import Batteries.Tactic.Basic
85+
public import Batteries.Tactic.Case
86+
public import Batteries.Tactic.Congr
87+
public import Batteries.Tactic.Exact
88+
public import Batteries.Tactic.HelpCmd
89+
public import Batteries.Tactic.Init
90+
public import Batteries.Tactic.Instances
91+
public import Batteries.Tactic.Lemma
92+
public import Batteries.Tactic.Lint
93+
public import Batteries.Tactic.Lint.Basic
94+
public import Batteries.Tactic.Lint.Frontend
95+
public import Batteries.Tactic.Lint.Misc
96+
public import Batteries.Tactic.Lint.Simp
97+
public import Batteries.Tactic.Lint.TypeClass
98+
public import Batteries.Tactic.NoMatch
99+
public import Batteries.Tactic.OpenPrivate
100+
public import Batteries.Tactic.PermuteGoals
101+
public import Batteries.Tactic.PrintDependents
102+
public import Batteries.Tactic.PrintOpaques
103+
public import Batteries.Tactic.PrintPrefix
104+
public import Batteries.Tactic.SeqFocus
105+
public import Batteries.Tactic.ShowUnused
106+
public import Batteries.Tactic.SqueezeScope
107+
public import Batteries.Tactic.Trans
108+
public import Batteries.Tactic.Unreachable
109+
public import Batteries.Util.Cache
110+
public import Batteries.Util.ExtendedBinder
111+
public import Batteries.Util.LibraryNote
112+
public import Batteries.Util.Panic
113+
public import Batteries.Util.Pickle
114+
public import Batteries.Util.ProofWanted
115+
public import Batteries.WF

‎Batteries/Classes/Cast.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,11 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro, Gabriel Ebner
55
-/
6-
import Batteries.Util.LibraryNote
6+
module
7+
8+
public import Batteries.Util.LibraryNote
9+
10+
@[expose] public section
711

812
library_note "coercion into rings"
913
/--

‎Batteries/Classes/Deprecated.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,11 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
6-
import Batteries.Classes.Order
6+
module
7+
8+
public import Batteries.Classes.Order
9+
10+
@[expose] public section
711

812
/-! Deprecated Batteries comparison classes
913

‎Batteries/Classes/Order.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,12 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
6-
import Batteries.Tactic.Basic
7-
import Batteries.Tactic.SeqFocus
6+
module
7+
8+
public import Batteries.Tactic.Basic
9+
public import Batteries.Tactic.SeqFocus
10+
11+
@[expose] public section
812

913
theorem lexOrd_def [Ord α] [Ord β] :
1014
(lexOrd : Ord (α × β)).compare = compareLex (compareOn (·.1)) (compareOn (·.2)) := rfl

‎Batteries/Classes/RatCast.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,9 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro, Gabriel Ebner
55
-/
6+
module
7+
8+
@[expose] public section
69

710
/-- Type class for the canonical homomorphism `Rat → K`. -/
811
class RatCast (K : Type u) where

‎Batteries/Classes/SatisfiesM.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,12 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro, Kim Morrison
55
-/
6-
import Batteries.Lean.EStateM
7-
import Batteries.Lean.Except
6+
module
7+
8+
public import Batteries.Lean.EStateM
9+
public import Batteries.Lean.Except
10+
11+
@[expose] public section
812

913
/-!
1014
## SatisfiesM

‎Batteries/CodeAction.lean‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1-
import Batteries.CodeAction.Attr
2-
import Batteries.CodeAction.Basic
3-
import Batteries.CodeAction.Misc
4-
import Batteries.CodeAction.Match
1+
module
2+
3+
public import Batteries.CodeAction.Attr
4+
public import Batteries.CodeAction.Basic
5+
public import Batteries.CodeAction.Misc
6+
public import Batteries.CodeAction.Match

‎Batteries/CodeAction/Attr.lean‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,12 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
6-
import Lean.Server.CodeActions.Basic
6+
module
7+
8+
public import Lean.Server.CodeActions.Basic
9+
public import Lean.Compiler.IR.CompilerM
10+
11+
@[expose] public section
712

813
/-!
914
# Initial setup for code action attributes

‎Batteries/CodeAction/Basic.lean‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,15 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
6-
import Lean.Elab.BuiltinTerm
7-
import Lean.Elab.BuiltinNotation
8-
import Lean.Server.InfoUtils
9-
import Lean.Server.CodeActions.Provider
10-
import Batteries.CodeAction.Attr
6+
module
7+
8+
public meta import Lean.Elab.BuiltinTerm
9+
public meta import Lean.Elab.BuiltinNotation
10+
public meta import Lean.Server.InfoUtils
11+
public meta import Lean.Server.CodeActions.Provider
12+
public meta import Batteries.CodeAction.Attr
13+
14+
public meta section
1115

1216
/-!
1317
# Initial setup for code actions

‎Batteries/CodeAction/Deprecated.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,11 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
6-
import Lean.Server.CodeActions.Provider
6+
module
7+
8+
public meta import Lean.Server.CodeActions.Provider
9+
10+
public meta section
711

812
/-!
913
# Code action for @[deprecated] replacements

0 commit comments

Comments
 (0)