forked from leanprover-community/batteries
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Std.lean
106 lines (106 loc) · 2.86 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
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.Control.ForInStep
import Std.Control.ForInStep.Basic
import Std.Control.ForInStep.Lemmas
import Std.Data.Array.Basic
import Std.Data.Array.Init.Basic
import Std.Data.Array.Init.Lemmas
import Std.Data.Array.Lemmas
import Std.Data.Array.Merge
import Std.Data.AssocList
import Std.Data.BinomialHeap
import Std.Data.Char
import Std.Data.DList
import Std.Data.Fin.Lemmas
import Std.Data.HashMap
import Std.Data.HashMap.Basic
import Std.Data.HashMap.WF
import Std.Data.Int.Basic
import Std.Data.Int.DivMod
import Std.Data.Int.Lemmas
import Std.Data.List.Basic
import Std.Data.List.Init.Lemmas
import Std.Data.List.Lemmas
import Std.Data.Nat.Basic
import Std.Data.Nat.Gcd
import Std.Data.Nat.Lemmas
import Std.Data.Option.Basic
import Std.Data.Option.Init.Lemmas
import Std.Data.Option.Lemmas
import Std.Data.Ord
import Std.Data.PairingHeap
import Std.Data.Prod.Lex
import Std.Data.RBMap
import Std.Data.RBMap.Alter
import Std.Data.RBMap.Basic
import Std.Data.RBMap.Lemmas
import Std.Data.RBMap.WF
import Std.Data.Rat
import Std.Data.Rat.Basic
import Std.Data.Rat.Lemmas
import Std.Data.String
import Std.Data.String.Basic
import Std.Data.String.Lemmas
import Std.Lean.AttributeExtra
import Std.Lean.Command
import Std.Lean.Delaborator
import Std.Lean.Expr
import Std.Lean.HashMap
import Std.Lean.HashSet
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.LCtx
import Std.Lean.Meta.SavedState
import Std.Lean.Meta.UnusedNames
import Std.Lean.MonadBacktrack
import Std.Lean.NameMapAttribute
import Std.Lean.Parser
import Std.Lean.PersistentHashMap
import Std.Lean.PersistentHashSet
import Std.Lean.Tactic
import Std.Lean.TagAttribute
import Std.Linter
import Std.Linter.UnnecessarySeqFocus
import Std.Linter.UnreachableTactic
import Std.Logic
import Std.Tactic.Basic
import Std.Tactic.ByCases
import Std.Tactic.CoeExt
import Std.Tactic.Congr
import Std.Tactic.Ext
import Std.Tactic.Ext.Attr
import Std.Tactic.GuardExpr
import Std.Tactic.HaveI
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.Ext
import Std.Tactic.NormCast.Lemmas
import Std.Tactic.OpenPrivate
import Std.Tactic.RCases
import Std.Tactic.SeqFocus
import Std.Tactic.ShowTerm
import Std.Tactic.SimpTrace
import Std.Tactic.Simpa
import Std.Tactic.SqueezeScope
import Std.Tactic.TryThis
import Std.Tactic.Unreachable
import Std.Util.ExtendedBinder
import Std.Util.LibraryNote
import Std.Util.TermUnsafe
import Std.WF