-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathFierceNerdsUtil.lean
More file actions
121 lines (121 loc) · 6.09 KB
/
FierceNerdsUtil.lean
File metadata and controls
121 lines (121 loc) · 6.09 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
117
118
119
120
121
import FierceNerdsUtil.Array_fun_basic
import FierceNerdsUtil.Array_fun_sep
import FierceNerdsUtil.Char_fun
import FierceNerdsUtil.Except_coe_in
import FierceNerdsUtil.Except_coe_out
import FierceNerdsUtil.Except_fun
import FierceNerdsUtil.False_theorem
import FierceNerdsUtil.FierceNerds.Example.Library
import FierceNerdsUtil.FierceNerds.Example.Library.Author
import FierceNerdsUtil.FierceNerds.Example.Library.Book
import FierceNerdsUtil.FierceNerds.Geometry
import FierceNerdsUtil.FierceNerds.Geometry.Cuboid_type
import FierceNerdsUtil.FierceNerds.Geometry.HIntersects_class
import FierceNerdsUtil.FierceNerds.Geometry.Intersects_class
import FierceNerdsUtil.FierceNerds.Geometry.Line_type
import FierceNerdsUtil.FierceNerds.Geometry.Point_type
import FierceNerdsUtil.FierceNerds.Geometry.Sphere_type
import FierceNerdsUtil.FierceNerds.OptParse.ArgParserV1_type
import FierceNerdsUtil.FierceNerds.OptParse.ArgParsersLawsV1_type
import FierceNerdsUtil.FierceNerds.OptParse.ArgParsersV1_type
import FierceNerdsUtil.FierceNerds.OptParse.Drafts
import FierceNerdsUtil.FierceNerds.OptParse.EStateMV2_type
import FierceNerdsUtil.FierceNerds.OptParse.ErrorV1_type
import FierceNerdsUtil.FierceNerds.OptParse.Input_type
import FierceNerdsUtil.FierceNerds.OptParse.Main_fun
import FierceNerdsUtil.FierceNerds.OptParse.MergeV1_type
import FierceNerdsUtil.FierceNerds.OptParse.Merge_instance
import FierceNerdsUtil.FierceNerds.OptParse.Names_type
import FierceNerdsUtil.FierceNerds.OptParse.OptParserV1_type
import FierceNerdsUtil.FierceNerds.OptParse.OptParsersLawsV1_type
import FierceNerdsUtil.FierceNerds.OptParse.OptParsersV1_type
import FierceNerdsUtil.FierceNerds.OptParse.ParseV1_type
import FierceNerdsUtil.FierceNerds.OptParse.ParseV2_type
import FierceNerdsUtil.FierceNerds.OptParse.Parse_instance
import FierceNerdsUtil.FierceNerds.OptParse.StateV2_type
import FierceNerdsUtil.FierceNerds.Util.AssocList_all
import FierceNerdsUtil.FierceNerds.Util.BEqBy_type
import FierceNerdsUtil.FierceNerds.Util.Bag_all
import FierceNerdsUtil.FierceNerds.Util.BagsUnique_all
import FierceNerdsUtil.FierceNerds.Util.Bags_all
import FierceNerdsUtil.FierceNerds.Util.ChainwiseList_type
import FierceNerdsUtil.FierceNerds.Util.ChainwiseLists_type
import FierceNerdsUtil.FierceNerds.Util.Collection_all
import FierceNerdsUtil.FierceNerds.Util.Cyclical_all
import FierceNerdsUtil.FierceNerds.Util.EqBy_all
import FierceNerdsUtil.FierceNerds.Util.Filter_all
import FierceNerdsUtil.FierceNerds.Util.FinLE_type
import FierceNerdsUtil.FierceNerds.Util.FinNZ_type
import FierceNerdsUtil.FierceNerds.Util.Fintype_type
import FierceNerdsUtil.FierceNerds.Util.HasId_class
import FierceNerdsUtil.FierceNerds.Util.HasUid_class
import FierceNerdsUtil.FierceNerds.Util.HashMap_all
import FierceNerdsUtil.FierceNerds.Util.Id_type
import FierceNerdsUtil.FierceNerds.Util.Injective_def
import FierceNerdsUtil.FierceNerds.Util.Interval_type
import FierceNerdsUtil.FierceNerds.Util.Issue_coe_from
import FierceNerdsUtil.FierceNerds.Util.Issue_fun
import FierceNerdsUtil.FierceNerds.Util.Issue_type
import FierceNerdsUtil.FierceNerds.Util.LawfulLE_class
import FierceNerdsUtil.FierceNerds.Util.Lens_type
import FierceNerdsUtil.FierceNerds.Util.Limited_all
import FierceNerdsUtil.FierceNerds.Util.List.AllEq
import FierceNerdsUtil.FierceNerds.Util.List.Chainwise.Example
import FierceNerdsUtil.FierceNerds.Util.List.Loop
import FierceNerdsUtil.FierceNerds.Util.List.Macro
import FierceNerdsUtil.FierceNerds.Util.ListPredWithEmptyPass_type
import FierceNerdsUtil.FierceNerds.Util.ListUniqueBy_example
import FierceNerdsUtil.FierceNerds.Util.ListUniqueBy_fun
import FierceNerdsUtil.FierceNerds.Util.ListUniqueBy_instance
import FierceNerdsUtil.FierceNerds.Util.ListUniqueBy_type
import FierceNerdsUtil.FierceNerds.Util.Mapper_type
import FierceNerdsUtil.FierceNerds.Util.Mutator_type
import FierceNerdsUtil.FierceNerds.Util.NodeV1_type
import FierceNerdsUtil.FierceNerds.Util.NodeV2_type
import FierceNerdsUtil.FierceNerds.Util.NonEmptyList_all
import FierceNerdsUtil.FierceNerds.Util.Optimal_type
import FierceNerdsUtil.FierceNerds.Util.PairwiseBy_example
import FierceNerdsUtil.FierceNerds.Util.PairwiseBy_type
import FierceNerdsUtil.FierceNerds.Util.Point_all
import FierceNerdsUtil.FierceNerds.Util.Pos_all
import FierceNerdsUtil.FierceNerds.Util.Position2D
import FierceNerdsUtil.FierceNerds.Util.Projections_type
import FierceNerdsUtil.FierceNerds.Util.Rate_type
import FierceNerdsUtil.FierceNerds.Util.Rel_type
import FierceNerdsUtil.FierceNerds.Util.SIUnitAsRat_rest
import FierceNerdsUtil.FierceNerds.Util.SIUnit_rest
import FierceNerdsUtil.FierceNerds.Util.SIUnit_thoughts
import FierceNerdsUtil.FierceNerds.Util.SIUnit_type
import FierceNerdsUtil.FierceNerds.Util.Scaffold
import FierceNerdsUtil.FierceNerds.Util.SortedBy_type
import FierceNerdsUtil.FierceNerds.Util.SubtypeSort_type
import FierceNerdsUtil.FierceNerds.Util.Thought_macro
import FierceNerdsUtil.FierceNerds.Util.Thought_type
import FierceNerdsUtil.FierceNerds.Util.Thoughts_macro
import FierceNerdsUtil.FierceNerds.Util.Thoughts_type
import FierceNerdsUtil.FierceNerds.Util.ToRatId_class
import FierceNerdsUtil.FierceNerds.Util.ToRat_class
import FierceNerdsUtil.FierceNerds.Util.ToSort_class
import FierceNerdsUtil.FierceNerds.Util.Todo_fun
import FierceNerdsUtil.FierceNerds.Util.TypedValue_type
import FierceNerdsUtil.FierceNerds.Util.Uid_type
import FierceNerdsUtil.FierceNerds.Util.UniqueByUid_type
import FierceNerdsUtil.FierceNerds.Util.UniqueBy_theorem
import FierceNerdsUtil.FierceNerds.Util.UniqueBy_type
import FierceNerdsUtil.FierceNerds.Util.Vector_all
import FierceNerdsUtil.IO_fun_basic
import FierceNerdsUtil.List_fun_basic
import FierceNerdsUtil.List_fun_is
import FierceNerdsUtil.List_fun_sep
import FierceNerdsUtil.List_theorem
import FierceNerdsUtil.NonemptyInterval_fun
import FierceNerdsUtil.Option_abbrev
import FierceNerdsUtil.Pred_type
import FierceNerdsUtil.Rat_instance
import FierceNerdsUtil.String_coe
import FierceNerdsUtil.String_fun
import FierceNerdsUtil.Subtype_abbrev
import FierceNerdsUtil.System.FileContent_fun
import FierceNerdsUtil.System.FileContent_type
import FierceNerdsUtil.System.FilePath_example_level
import FierceNerdsUtil.System.FilePath_fun