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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
|
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>mathcomp.ssreflect.ssrnotations</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library mathcomp.ssreflect.ssrnotations</h1>
<div class="code">
<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/>
Distributed under the terms of CeCILL-B. *)</span><br/>
<br/>
</div>
<div class="doc">
<ul class="doclist">
<li> Reserved notation for various arithmetic and algebraic operations:
e. [a1, ..., a_n] evaluation (e.g., polynomials).
e`<i>i indexing (number list, integer pi-part).
x^-1 inverse (group, field).
x *+ n, x *- n integer multiplier (modules and rings).
x ^+ n, x ^- n integer exponent (groups and rings).
x *: A, A :* x external product (scaling/module product in rings,
left/right cosets in groups).
A :&: B intersection (of sets, groups, subspaces, ...).
A :|: B, a |: B union, union with a singleton (of sets).
A :\: B, A :\ b relative complement (of sets, subspaces, ...).
<tt>A</tt>, < [a]> generated group/subspace, generated cycle/line.
'C[x], 'C_A[x] point centralisers (in groups and F-algebras).
'C(A), 'C_B(A) centralisers (in groups and matrix and F_algebras).
'Z(A) centers (in groups and matrix and F-algebras).
m %/ d, m %% d Euclidean division and remainder (nat, polynomials).
d %| m Euclidean divisibility (nat, polynomial).
m = n % [mod d] equality mod d (also defined for <>, ==, and !=).
e^`(n) nth formal derivative (groups, polynomials).
e^` simple formal derivative (polynomials only).
`|x| norm, absolute value, distance (rings, int, nat).
x <= y ?= iff C x is less than y, and equal iff C holds (nat, rings).
x <= y :> T, etc cast comparison (rings, all comparison operators).
[rec a1, ..., an] standard shorthand for hidden recursor (see prime.v).
The interpretation of these notations is not defined here, but the
declarations help maintain consistency across the library.
<div class="paragraph"> </div>
Reserved notation for evaluation
</li>
</ul>
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "e .[ x ]"<br/>
(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "e .[ x ]").<br/>
<br/>
<span class="id" title="keyword">Reserved Notation</span> "e .[ x1 , x2 , .. , xn ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>,<br/>
<span class="id" title="var">format</span> "e '[ ' .[ x1 , '/' x2 , '/' .. , '/' xn ] ']'").<br/>
<br/>
</div>
<div class="doc">
Reserved notation for subscripting and superscripting
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "s `_ i" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3, <span class="id" title="var">i</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>,<br/>
<span class="id" title="var">format</span> "s `_ i").<br/>
<span class="id" title="keyword">Reserved Notation</span> "x ^-1" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "x ^-1").<br/>
<br/>
</div>
<div class="doc">
Reserved notation for integer multipliers and exponents
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "x *+ n" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "x *- n" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "x ^+ n" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 29, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "x ^- n" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 29, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<br/>
</div>
<div class="doc">
Reserved notation for external multiplication.
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "x *: A" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/>
<span class="id" title="keyword">Reserved Notation</span> "A :* x" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/>
<br/>
</div>
<div class="doc">
Reserved notation for set-theretic operations.
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "A :&: B" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 48, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "A :|: B" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 52, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "a |: A" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 52, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "A :\: B" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "A :\ b" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<br/>
</div>
<div class="doc">
Reserved notation for generated structures
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "<< A >>" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "<< A >>").<br/>
<span class="id" title="keyword">Reserved Notation</span> "<[ a ] >" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "<[ a ] >").<br/>
<br/>
</div>
<div class="doc">
Reserved notation for centralisers and centers.
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "''C' [ x ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "''C' [ x ]").<br/>
<span class="id" title="keyword">Reserved Notation</span> "''C_' A [ x ]"<br/>
(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">A</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''C_' A [ x ]").<br/>
<span class="id" title="keyword">Reserved Notation</span> "''C' ( A )" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "''C' ( A )").<br/>
<span class="id" title="keyword">Reserved Notation</span> "''C_' B ( A )"<br/>
(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">B</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''C_' B ( A )").<br/>
<span class="id" title="keyword">Reserved Notation</span> "''Z' ( A )" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "''Z' ( A )").<br/>
</div>
<div class="doc">
Compatibility with group action centraliser notation.
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "''C_' ( A ) [ x ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "''C_' ( B ) ( A )" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>).<br/>
<br/>
</div>
<div class="doc">
Reserved notation for Euclidean division and divisibility.
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "m %/ d" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40, <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "m %% d" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40, <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "m %| d" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "m = n %[mod d ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/>
<span class="id" title="var">format</span> "'[hv ' m '/' = n '/' %[mod d ] ']'").<br/>
<span class="id" title="keyword">Reserved Notation</span> "m == n %[mod d ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/>
<span class="id" title="var">format</span> "'[hv ' m '/' == n '/' %[mod d ] ']'").<br/>
<span class="id" title="keyword">Reserved Notation</span> "m <> n %[mod d ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/>
<span class="id" title="var">format</span> "'[hv ' m '/' <> n '/' %[mod d ] ']'").<br/>
<span class="id" title="keyword">Reserved Notation</span> "m != n %[mod d ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/>
<span class="id" title="var">format</span> "'[hv ' m '/' != n '/' %[mod d ] ']'").<br/>
<br/>
</div>
<div class="doc">
Reserved notation for derivatives.
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "a ^` " (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "a ^` ").<br/>
<span class="id" title="keyword">Reserved Notation</span> "a ^` ( n )" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "a ^` ( n )").<br/>
<br/>
</div>
<div class="doc">
Reserved notation for absolute value.
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "`| x |" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99, <span class="id" title="var">format</span> "`| x |").<br/>
<br/>
</div>
<div class="doc">
Reserved notation for conditional comparison
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "x <= y ?= 'iff' c" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span>, <span class="id" title="var">c</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/>
<span class="id" title="var">format</span> "x '[hv' <= y '/' ?= 'iff' c ']'").<br/>
<br/>
</div>
<div class="doc">
Reserved notation for cast comparison.
</div>
<div class="code">
<span class="id" title="keyword">Reserved Notation</span> "x <= y :> T" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "x >= y :> T" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "x < y :> T" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "x > y :> T" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>).<br/>
<span class="id" title="keyword">Reserved Notation</span> "x <= y ?= 'iff' c :> T" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span>, <span class="id" title="var">c</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/>
<span class="id" title="var">format</span> "x '[hv' <= y '/' ?= 'iff' c :> T ']'").<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
|
