diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.ssrnotations.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.ssrnotations.html | 221 |
1 files changed, 0 insertions, 221 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.ssrnotations.html b/docs/htmldoc/mathcomp.ssreflect.ssrnotations.html deleted file mode 100644 index 22be516..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.ssrnotations.html +++ /dev/null @@ -1,221 +0,0 @@ -<!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 |