diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.ssreflect.ssreflect.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.ssreflect.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.ssreflect.html | 143 |
1 files changed, 0 insertions, 143 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.ssreflect.html b/docs/htmldoc/mathcomp.ssreflect.ssreflect.html deleted file mode 100644 index 7772d24..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.ssreflect.html +++ /dev/null @@ -1,143 +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.ssreflect</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.ssreflect.ssreflect</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"> - Local additions: - nonPropType == an interface for non-Prop Types: a nonPropType coerces - to a Type, and only types that do <i>not</i> have sort - Prop are canonical nonPropType instances. This is - useful for applied views. -> This will become standard with the Coq v8.11 SSReflect core library. - deprecate old new == new, but warning that old is deprecated and new - should be used instead. -> Usage: Notation old := (deprecate old new) (only parsing). -> Caveat: deprecate old new only inherits new's maximal implicits; - on-demand implicits should be added after : (deprecate old new _). -> Caveat 2: if premises or conclusions need to be adjusted, of for - non-prenex implicits, use the idiom: - Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...) - _ ... _) (only printing). - where all the implicit a_i's occur first, and correspond to the - trailing <i>'s, making sure deprecate old new is fully applied and - there are <i>no implicits</i> inside the (fun .. => ..) expression. This - is to avoid triggering a bug in SSReflect elaboration that is - triggered by such evars under binders. - Import Deprecation.Silent :: turn off deprecation warning messages. - Import Deprecation.Reject :: raise an error instead of only warning. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Module</span> <a name="NonPropType"><span class="id" title="module">NonPropType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="NonPropType.call_of"><span class="id" title="record">call_of</span></a> (<span class="id" title="var">condition</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>) (<span class="id" title="var">result</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>) := <a name="NonPropType.Call"><span class="id" title="constructor">Call</span></a> {<a name="NonPropType.callee"><span class="id" title="projection">callee</span></a> : <span class="id" title="keyword">Type</span>}.<br/> -<span class="id" title="keyword">Definition</span> <a name="NonPropType.maybeProp"><span class="id" title="definition">maybeProp</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="NonPropType.call"><span class="id" title="definition">call</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Call"><span class="id" title="constructor">Call</span></a> (<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.maybeProp"><span class="id" title="definition">maybeProp</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="NonPropType.test_of"><span class="id" title="record">test_of</span></a> (<span class="id" title="var">result</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>) := <a name="NonPropType.Test"><span class="id" title="constructor">Test</span></a> {<a name="NonPropType.condition"><span class="id" title="projection">condition</span></a> :> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>}.<br/> -<span class="id" title="keyword">Definition</span> <a name="NonPropType.test_Prop"><span class="id" title="definition">test_Prop</span></a> (<span class="id" title="var">P</span> : <span class="id" title="keyword">Prop</span>) := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Test"><span class="id" title="constructor">Test</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> (<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.maybeProp"><span class="id" title="definition">maybeProp</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#P"><span class="id" title="variable">P</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="NonPropType.test_negative"><span class="id" title="definition">test_negative</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Test"><span class="id" title="constructor">Test</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="NonPropType.type"><span class="id" title="record">type</span></a> :=<br/> - <a name="NonPropType.Check"><span class="id" title="constructor">Check</span></a> {<a name="NonPropType.result"><span class="id" title="projection">result</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>; <a name="NonPropType.test"><span class="id" title="projection">test</span></a> : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.test_of"><span class="id" title="record">test_of</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#result"><span class="id" title="method">result</span></a>; <a name="NonPropType.frame"><span class="id" title="projection">frame</span></a> : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.call_of"><span class="id" title="record">call_of</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#test"><span class="id" title="method">test</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#result"><span class="id" title="method">result</span></a>}.<br/> -<span class="id" title="keyword">Definition</span> <a name="NonPropType.check"><span class="id" title="definition">check</span></a> <span class="id" title="var">result</span> <span class="id" title="var">test</span> <span class="id" title="var">frame</span> := @<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Check"><span class="id" title="constructor">Check</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#result"><span class="id" title="variable">result</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#test"><span class="id" title="variable">test</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#frame"><span class="id" title="variable">frame</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="NonPropType.Exports"><span class="id" title="module">Exports</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">call</span>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">test_Prop</span>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">test_negative</span>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">check</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="NonPropType.Exports.nonPropType"><span class="id" title="abbreviation">nonPropType</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.type"><span class="id" title="record">type</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">callee</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">call_of</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">Sortclass</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">frame</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">type</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">call_of</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="NonPropType.Exports.notProp"><span class="id" title="abbreviation">notProp</span></a> <span class="id" title="var">T</span> := (@<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.check"><span class="id" title="definition">check</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.test_negative"><span class="id" title="definition">test_negative</span></a> (<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.call"><span class="id" title="definition">call</span></a> <span class="id" title="var">T</span>)).<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Exports"><span class="id" title="module">Exports</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType"><span class="id" title="module">NonPropType</span></a>.<br/> -<span class="id" title="keyword">Export</span> <span class="id" title="var">NonPropType.Exports</span>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="Deprecation"><span class="id" title="module">Deprecation</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Deprecation.hidden"><span class="id" title="definition">hidden</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Deprecation.exposed"><span class="id" title="definition">exposed</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) & <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Deprecation.hide"><span class="id" title="definition">hide</span></a> <span class="id" title="var">T</span> <span class="id" title="var">u</span> (<span class="id" title="var">v</span> : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.exposed"><span class="id" title="definition">exposed</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#u"><span class="id" title="variable">u</span></a>) : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hidden"><span class="id" title="definition">hidden</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#v"><span class="id" title="variable">v</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Ltac</span> <span class="id" title="var">warn</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> :=<br/> - <span class="id" title="tactic">idtac</span> "Warning:" <span class="id" title="var">old_id</span> "is deprecated; use" <span class="id" title="var">new_id</span> "instead".<br/> - -<br/> -<span class="id" title="keyword">Ltac</span> <span class="id" title="var">stop</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> :=<br/> - <span class="id" title="tactic">fail</span> 1 "Error:" <span class="id" title="var">old_id</span> "is deprecated; use" <span class="id" title="var">new_id</span> "instead".<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="Deprecation.hinted"><span class="id" title="record">hinted</span></a> := <a name="Deprecation.Hint"><span class="id" title="constructor">Hint</span></a> {<a name="Deprecation.statement"><span class="id" title="projection">statement</span></a>; <a name="Deprecation.hint"><span class="id" title="projection">hint</span></a> : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#statement"><span class="id" title="method">statement</span></a>}.<br/> -<span class="id" title="keyword">Ltac</span> <span class="id" title="var">check</span> <span class="id" title="var">cond</span> := <span class="id" title="keyword">let</span> <span class="id" title="var">test</span> := <span class="id" title="keyword">constr</span>:(<a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hint"><span class="id" title="projection">hint</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <span class="id" title="var">cond</span>) <span class="id" title="tactic">in</span> <span class="id" title="tactic">idtac</span>.<br/> - -<br/> -<span class="id" title="keyword">Variant</span> <a name="Deprecation.reject"><span class="id" title="inductive">reject</span></a> := <a name="Deprecation.Reject"><span class="id" title="constructor">Reject</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Deprecation.reject_hint"><span class="id" title="definition">reject_hint</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Hint"><span class="id" title="constructor">Hint</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.reject"><span class="id" title="inductive">reject</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Reject"><span class="id" title="constructor">Reject</span></a>.<br/> -<span class="id" title="keyword">Module</span> <a name="Deprecation.Reject"><span class="id" title="module">Reject</span></a>. <span class="id" title="var">Canonical</span> <span class="id" title="var">reject_hint</span>. <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Reject"><span class="id" title="module">Reject</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variant</span> <a name="Deprecation.silent"><span class="id" title="inductive">silent</span></a> := <a name="Deprecation.Silent"><span class="id" title="constructor">Silent</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Deprecation.silent_hint"><span class="id" title="definition">silent_hint</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Hint"><span class="id" title="constructor">Hint</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.silent"><span class="id" title="inductive">silent</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Silent"><span class="id" title="constructor">Silent</span></a>.<br/> -<span class="id" title="keyword">Module</span> <a name="Deprecation.Silent"><span class="id" title="module">Silent</span></a>. <span class="id" title="var">Canonical</span> <span class="id" title="var">silent_hint</span>. <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Silent"><span class="id" title="module">Silent</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Ltac</span> <span class="id" title="var">flag</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> :=<br/> - <span class="id" title="tactic">first</span> [<span class="id" title="var">check</span> <span class="id" title="var">reject</span>; <span class="id" title="var">stop</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> | <span class="id" title="var">check</span> <span class="id" title="var">silent</span> | <span class="id" title="var">warn</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span>].<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="Deprecation.Exports"><span class="id" title="module">Exports</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">hide</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">exposed</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">hidden</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Deprecation.Exports.deprecate"><span class="id" title="abbreviation">deprecate</span></a> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> :=<br/> - (<a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">hide</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> ⇒ <span class="id" title="keyword">ltac</span>:(<span class="id" title="var">flag</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span>; <span class="id" title="tactic">exact</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>)) <span class="id" title="var">new_id</span>)<br/> - (<span class="id" title="var">only</span> <span class="id" title="var">parsing</span>).<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Exports"><span class="id" title="module">Exports</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation"><span class="id" title="module">Deprecation</span></a>.<br/> -<span class="id" title="keyword">Export</span> <span class="id" title="var">Deprecation.Exports</span>.<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 |