forked from leanprover-community/batteries
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Std.lean
159 lines (159 loc) · 4.21 KB
/
Std.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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
import Std.Classes.BEq
import Std.Classes.Cast
import Std.Classes.Dvd
import Std.Classes.LawfulMonad
import Std.Classes.Order
import Std.Classes.RatCast
import Std.Classes.SetNotation
import Std.CodeAction
import Std.CodeAction.Attr
import Std.CodeAction.Basic
import Std.CodeAction.Deprecated
import Std.CodeAction.Misc
import Std.Control.ForInStep
import Std.Control.ForInStep.Basic
import Std.Control.ForInStep.Lemmas
import Std.Control.Lemmas
import Std.Control.Nondet.Basic
import Std.Data.Array
import Std.Data.AssocList
import Std.Data.BinomialHeap
import Std.Data.BitVec
import Std.Data.Bool
import Std.Data.ByteArray
import Std.Data.Char
import Std.Data.DList
import Std.Data.Fin
import Std.Data.HashMap
import Std.Data.Int
import Std.Data.Json
import Std.Data.LazyList
import Std.Data.List
import Std.Data.MLList
import Std.Data.Nat
import Std.Data.Option
import Std.Data.Ord
import Std.Data.PairingHeap
import Std.Data.Prod
import Std.Data.RBMap
import Std.Data.Range
import Std.Data.Rat
import Std.Data.String
import Std.Data.Sum
import Std.Data.UInt
import Std.Lean.AttributeExtra
import Std.Lean.Command
import Std.Lean.CoreM
import Std.Lean.Delaborator
import Std.Lean.Elab.Tactic
import Std.Lean.Except
import Std.Lean.Expr
import Std.Lean.Float
import Std.Lean.Format
import Std.Lean.HashMap
import Std.Lean.HashSet
import Std.Lean.IO.Process
import Std.Lean.InfoTree
import Std.Lean.Json
import Std.Lean.LocalContext
import Std.Lean.Meta.AssertHypotheses
import Std.Lean.Meta.Basic
import Std.Lean.Meta.Clear
import Std.Lean.Meta.DiscrTree
import Std.Lean.Meta.Expr
import Std.Lean.Meta.Inaccessible
import Std.Lean.Meta.InstantiateMVars
import Std.Lean.Meta.Iterator
import Std.Lean.Meta.LazyDiscrTree
import Std.Lean.Meta.SavedState
import Std.Lean.Meta.Simp
import Std.Lean.Meta.UnusedNames
import Std.Lean.MonadBacktrack
import Std.Lean.Name
import Std.Lean.NameMap
import Std.Lean.NameMapAttribute
import Std.Lean.Parser
import Std.Lean.PersistentHashMap
import Std.Lean.PersistentHashSet
import Std.Lean.Position
import Std.Lean.SMap
import Std.Lean.Syntax
import Std.Lean.System.IO
import Std.Lean.Tactic
import Std.Lean.TagAttribute
import Std.Lean.Util.EnvSearch
import Std.Lean.Util.Path
import Std.Linter
import Std.Linter.UnnecessarySeqFocus
import Std.Linter.UnreachableTactic
import Std.Logic
import Std.Tactic.Alias
import Std.Tactic.Basic
import Std.Tactic.ByCases
import Std.Tactic.Case
import Std.Tactic.Change
import Std.Tactic.Classical
import Std.Tactic.CoeExt
import Std.Tactic.Congr
import Std.Tactic.Exact
import Std.Tactic.Ext
import Std.Tactic.Ext.Attr
import Std.Tactic.FalseOrByContra
import Std.Tactic.GuardExpr
import Std.Tactic.GuardMsgs
import Std.Tactic.HaveI
import Std.Tactic.Init
import Std.Tactic.Instances
import Std.Tactic.LabelAttr
import Std.Tactic.LeftRight
import Std.Tactic.LibrarySearch
import Std.Tactic.Lint
import Std.Tactic.Lint.Basic
import Std.Tactic.Lint.Frontend
import Std.Tactic.Lint.Misc
import Std.Tactic.Lint.Simp
import Std.Tactic.Lint.TypeClass
import Std.Tactic.NoMatch
import Std.Tactic.NormCast
import Std.Tactic.NormCast.Ext
import Std.Tactic.NormCast.Lemmas
import Std.Tactic.Omega
import Std.Tactic.Omega.Coeffs.IntList
import Std.Tactic.Omega.Config
import Std.Tactic.Omega.Constraint
import Std.Tactic.Omega.Core
import Std.Tactic.Omega.Frontend
import Std.Tactic.Omega.Int
import Std.Tactic.Omega.IntList
import Std.Tactic.Omega.LinearCombo
import Std.Tactic.Omega.Logic
import Std.Tactic.Omega.MinNatAbs
import Std.Tactic.Omega.OmegaM
import Std.Tactic.OpenPrivate
import Std.Tactic.PermuteGoals
import Std.Tactic.PrintDependents
import Std.Tactic.PrintPrefix
import Std.Tactic.RCases
import Std.Tactic.Relation.Rfl
import Std.Tactic.Relation.Symm
import Std.Tactic.Replace
import Std.Tactic.RunCmd
import Std.Tactic.SeqFocus
import Std.Tactic.ShowTerm
import Std.Tactic.SimpTrace
import Std.Tactic.Simpa
import Std.Tactic.SolveByElim
import Std.Tactic.SolveByElim.Backtrack
import Std.Tactic.SqueezeScope
import Std.Tactic.TryThis
import Std.Tactic.Unreachable
import Std.Tactic.Where
import Std.Test.Internal.DummyLabelAttr
import Std.Util.Cache
import Std.Util.CheckTactic
import Std.Util.ExtendedBinder
import Std.Util.LibraryNote
import Std.Util.Pickle
import Std.Util.ProofWanted
import Std.Util.TermUnsafe
import Std.WF