diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.ssreflect.ssrnotations.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.ssrnotations.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.ssrnotations.html | 221 |
1 files changed, 221 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.ssrnotations.html b/docs/htmldoc/mathcomp.ssreflect.ssrnotations.html new file mode 100644 index 0000000..22be516 --- /dev/null +++ b/docs/htmldoc/mathcomp.ssreflect.ssrnotations.html @@ -0,0 +1,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>
\ No newline at end of file |