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