-
Notifications
You must be signed in to change notification settings - Fork 118
/
Copy pathStd.lean
107 lines (107 loc) · 2.78 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
import Std.Classes.BEq
import Std.Classes.Cast
import Std.Classes.Order
import Std.Classes.RatCast
import Std.Classes.SatisfiesM
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.LazyList
import Std.Data.List
import Std.Data.MLList
import Std.Data.Nat
import Std.Data.Option
import Std.Data.PairingHeap
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.Data.UnionFind
import Std.Lean.AttributeExtra
import Std.Lean.Delaborator
import Std.Lean.Except
import Std.Lean.Expr
import Std.Lean.Float
import Std.Lean.HashMap
import Std.Lean.HashSet
import Std.Lean.IO.Process
import Std.Lean.Json
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.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.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.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.Case
import Std.Tactic.Classical
import Std.Tactic.Congr
import Std.Tactic.Exact
import Std.Tactic.Init
import Std.Tactic.Instances
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.OpenPrivate
import Std.Tactic.PermuteGoals
import Std.Tactic.PrintDependents
import Std.Tactic.PrintPrefix
import Std.Tactic.SeqFocus
import Std.Tactic.ShowUnused
import Std.Tactic.SqueezeScope
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.WF