forked from leanprover-community/mathlib4
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathstyle-exceptions.txt
131 lines (131 loc) · 11.6 KB
/
style-exceptions.txt
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
Mathlib/Algebra/Ring/Basic.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Algebra/Ring/Basic.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Algebra/Ring/Basic.lean : line 12 : ERR_MOD : Module docstring missing, or too late
Mathlib/Algebra/Ring/Basic.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Algebra/Ring/Basic.lean : line 3 : ERR_COP : Malformed or missing copyright header
Mathlib/Algebra/Ring/Basic.lean : line 4 : ERR_COP : Malformed or missing copyright header
Mathlib/Algebra/Ring/Basic.lean : line 5 : ERR_COP : Malformed or missing copyright header
Mathlib/Algebra/Ring/Basic.lean : line 7 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Array/Basic.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Array/Basic.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Array/Basic.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Array/Basic.lean : line 4 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Array/Basic.lean : line 4 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/BinaryHeap.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/ByteArray.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/ByteArray.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/ByteArray.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/ByteArray.lean : line 3 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/ByteArray.lean : line 5 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/ByteArray.lean : line 5 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/Fin/Basic.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Fin/Basic.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Fin/Basic.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Fin/Basic.lean : line 3 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Fin/Basic.lean : line 4 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Fin/Basic.lean : line 5 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Fin/Basic.lean : line 7 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Fin/Basic.lean : line 7 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/Int/Basic.lean : line 235 : ERR_LIN : Line has more than 100 characters
Mathlib/Data/Int/Basic.lean : line 263 : ERR_LIN : Line has more than 100 characters
Mathlib/Data/Int/Basic.lean : line 269 : ERR_LIN : Line has more than 100 characters
Mathlib/Data/Int/Basic.lean : line 283 : ERR_LIN : Line has more than 100 characters
Mathlib/Data/Int/Basic.lean : line 286 : ERR_LIN : Line has more than 100 characters
Mathlib/Data/List/Basic.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 10 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/List/Basic.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 3 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 4 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 5 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 6 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 7 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Basic.lean : line 8 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Card.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/List/Card.lean : line 12 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/Nat/Basic.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Nat/Basic.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Nat/Basic.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Nat/Basic.lean : line 3 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Nat/Basic.lean : line 4 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Nat/Basic.lean : line 5 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Nat/Basic.lean : line 6 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Nat/Basic.lean : line 8 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Nat/Basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/String/Defs.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/String/Defs.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/String/Defs.lean : line 3 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/String/Defs.lean : line 3 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/String/Lemmas.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/String/Lemmas.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/String/Lemmas.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/String/Lemmas.lean : line 4 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/String/Lemmas.lean : line 4 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/UInt.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/UInt.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/UInt.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/UInt.lean : line 3 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/UInt.lean : line 4 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/UInt.lean : line 5 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/UInt.lean : line 7 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/UInt.lean : line 7 : ERR_MOD : Module docstring missing, or too late
Mathlib/Data/UnionFind.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Mathlib/Init/Algebra/Functions.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Init/Data/Int/Basic.lean : line 13 : ERR_MOD : Module docstring missing, or too late
Mathlib/Init/Data/Nat/Basic.lean : line 7 : ERR_MOD : Module docstring missing, or too late
Mathlib/Init/Data/Nat/Lemmas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Mathlib/Init/Function.lean : line 7 : ERR_MOD : Module docstring missing, or too late
Mathlib/Init/Logic.lean : line 16 : ERR_MOD : Module docstring missing, or too late
Mathlib/Init/Meta/WellFoundedTactics.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Mathlib/Lean/Exception.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Lean/Exception.lean : line 4 : ERR_AUT : Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'
Mathlib/Lean/Exception.lean : line 7 : ERR_MOD : Module docstring missing, or too late
Mathlib/Lean/Expr/ReplaceRec.lean : line 12 : ERR_MOD : Module docstring missing, or too late
Mathlib/Lean/LocalContext.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Mathlib/Logic/Equiv/LocalEquiv.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Logic/Equiv/LocalEquiv.lean : line 12 : ERR_MOD : Module docstring missing, or too late
Mathlib/Logic/Equiv/LocalEquiv.lean : line 4 : ERR_AUT : Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'
Mathlib/Logic/Equiv/MfldSimpsAttr.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Logic/Equiv/MfldSimpsAttr.lean : line 4 : ERR_AUT : Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'
Mathlib/Logic/Equiv/MfldSimpsAttr.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Mathport/Attributes.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Mathlib/Mathport/Rename.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Mathport/Syntax.lean : line 74 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Abstract.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/ApplyWith.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/ApplyWith.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/ApplyWith.lean : line 2 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/ApplyWith.lean : line 4 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/ApplyWith.lean : line 4 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/ByContra.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/ByContra.lean : line 4 : ERR_AUT : Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'
Mathlib/Tactic/ByContra.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/ClearExcept.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Coe.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Constructor.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Core.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Existsi.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Expect.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Have.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/LeftRight.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/NormCast/Tactic.lean : line 13 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/PermuteGoals.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/PrintPrefix.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/PushNeg.lean : line 13 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Recover.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Rename.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/RenameBVar.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Replace.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/RestateAxiom.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Set.lean : line 4 : ERR_AUT : Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'
Mathlib/Tactic/Set.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/SimpRw.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/Substs.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/Substs.lean : line 4 : ERR_AUT : Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'
Mathlib/Tactic/Substs.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Mathlib/Tactic/TypeCheck.lean : line 0 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/TypeCheck.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/TypeCheck.lean : line 3 : ERR_COP : Malformed or missing copyright header
Mathlib/Tactic/TypeCheck.lean : line 3 : ERR_MOD : Module docstring missing, or too late