blob: 7772d2455e076d2dbd67ac825671106f945c38c8 (
plain)
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
|
<!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>
|
