forked from leanprover-community/batteries
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Batteries.lean
104 lines (104 loc) · 3.33 KB
/
Batteries.lean
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
import Batteries.Classes.Cast
import Batteries.Classes.Order
import Batteries.Classes.RatCast
import Batteries.Classes.SatisfiesM
import Batteries.CodeAction
import Batteries.CodeAction.Attr
import Batteries.CodeAction.Basic
import Batteries.CodeAction.Deprecated
import Batteries.CodeAction.Misc
import Batteries.Control.ForInStep
import Batteries.Control.ForInStep.Basic
import Batteries.Control.ForInStep.Lemmas
import Batteries.Control.Lemmas
import Batteries.Control.Nondet.Basic
import Batteries.Data.Array
import Batteries.Data.AssocList
import Batteries.Data.BinaryHeap
import Batteries.Data.BinomialHeap
import Batteries.Data.ByteArray
import Batteries.Data.ByteSubarray
import Batteries.Data.Char
import Batteries.Data.DList
import Batteries.Data.Fin
import Batteries.Data.FloatArray
import Batteries.Data.HashMap
import Batteries.Data.LazyList
import Batteries.Data.List
import Batteries.Data.MLList
import Batteries.Data.Nat
import Batteries.Data.PairingHeap
import Batteries.Data.RBMap
import Batteries.Data.Range
import Batteries.Data.Rat
import Batteries.Data.String
import Batteries.Data.Sum
import Batteries.Data.UInt
import Batteries.Data.UnionFind
import Batteries.Data.Vector
import Batteries.Lean.AttributeExtra
import Batteries.Lean.Delaborator
import Batteries.Lean.Except
import Batteries.Lean.Expr
import Batteries.Lean.Float
import Batteries.Lean.HashMap
import Batteries.Lean.HashSet
import Batteries.Lean.IO.Process
import Batteries.Lean.Json
import Batteries.Lean.Meta.Basic
import Batteries.Lean.Meta.DiscrTree
import Batteries.Lean.Meta.Expr
import Batteries.Lean.Meta.Inaccessible
import Batteries.Lean.Meta.InstantiateMVars
import Batteries.Lean.Meta.SavedState
import Batteries.Lean.Meta.Simp
import Batteries.Lean.Meta.UnusedNames
import Batteries.Lean.MonadBacktrack
import Batteries.Lean.NameMap
import Batteries.Lean.NameMapAttribute
import Batteries.Lean.PersistentHashMap
import Batteries.Lean.PersistentHashSet
import Batteries.Lean.Position
import Batteries.Lean.Syntax
import Batteries.Lean.System.IO
import Batteries.Lean.TagAttribute
import Batteries.Lean.Util.EnvSearch
import Batteries.Linter
import Batteries.Linter.UnnecessarySeqFocus
import Batteries.Linter.UnreachableTactic
import Batteries.Logic
import Batteries.StdDeprecations
import Batteries.Tactic.Alias
import Batteries.Tactic.Basic
import Batteries.Tactic.Case
import Batteries.Tactic.Classical
import Batteries.Tactic.Congr
import Batteries.Tactic.Exact
import Batteries.Tactic.HelpCmd
import Batteries.Tactic.Init
import Batteries.Tactic.Instances
import Batteries.Tactic.Lemma
import Batteries.Tactic.Lint
import Batteries.Tactic.Lint.Basic
import Batteries.Tactic.Lint.Frontend
import Batteries.Tactic.Lint.Misc
import Batteries.Tactic.Lint.Simp
import Batteries.Tactic.Lint.TypeClass
import Batteries.Tactic.NoMatch
import Batteries.Tactic.OpenPrivate
import Batteries.Tactic.PermuteGoals
import Batteries.Tactic.PrintDependents
import Batteries.Tactic.PrintPrefix
import Batteries.Tactic.SeqFocus
import Batteries.Tactic.ShowUnused
import Batteries.Tactic.SqueezeScope
import Batteries.Tactic.Unreachable
import Batteries.Tactic.Where
import Batteries.Test.Internal.DummyLabelAttr
import Batteries.Util.Cache
import Batteries.Util.ExtendedBinder
import Batteries.Util.LibraryNote
import Batteries.Util.Panic
import Batteries.Util.Pickle
import Batteries.Util.ProofWanted
import Batteries.WF