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
|
<!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.ssrbool</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library mathcomp.ssreflect.ssrbool</h1>
<div class="code">
<br/>
</div>
<div class="doc">
Local additions:
{pred T} == a type convertible to pred T but that presents the
pred_sort coercion class.
PredType toP == the predType structure for toP : A -> pred T.
relpre f r == the preimage of r by f, simplifying to r (f x) (f y).
> These will become part of the core SSReflect library with Coq 8.11.
This file also anticipates a v8.11 change in the definition of simpl_pred
to T -> simpl_pred T. This change ensures that inE expands the definition
of r : simpl_rel along with the \in, when rewriting in y \in r x.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Notation</span> <a name="64f8873130736b599801d4930af00e74"><span class="id" title="notation">"</span></a>{ 'pred' T }" := (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred_sort"><span class="id" title="projection">pred_sort</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <span class="id" title="var">T</span>)) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
<span class="id" title="var">format</span> "{ 'pred' T }") : <span class="id" title="var">type_scope</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="simpl_pred_sortE"><span class="id" title="lemma">simpl_pred_sortE</span></a> <span class="id" title="var">T</span> (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#SimplPred"><span class="id" title="definition">SimplPred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#p"><span class="id" title="variable">p</span></a> <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> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#p"><span class="id" title="variable">p</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a name="inE"><span class="id" title="definition">inE</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#inE"><span class="id" title="definition">inE</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#simpl_pred_sortE"><span class="id" title="lemma">simpl_pred_sortE</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="PredType"><span class="id" title="definition">PredType</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">T</span> <span class="id" title="var">pT</span>, <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="mathcomp.ssreflect.ssrbool.html#pT"><span class="id" title="variable">pT</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.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.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.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.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Defined</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="simpl_rel"><span class="id" title="definition">simpl_rel</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.ssrbool.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.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#simpl_pred"><span class="id" title="definition">simpl_pred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a name="SimplRel"><span class="id" title="definition">SimplRel</span></a> {<span class="id" title="var">T</span>} (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#simpl_rel"><span class="id" title="definition">simpl_rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#SimplPred"><span class="id" title="definition">SimplPred</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#x"><span class="id" title="variable">x</span></a>).<br/>
<span class="id" title="keyword">Coercion</span> <span class="id" title="var">rel_of_simpl_rel</span> <span class="id" title="var">T</span> (<span class="id" title="var">sr</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#simpl_rel"><span class="id" title="definition">simpl_rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#sr"><span class="id" title="variable">sr</span></a>.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a name="fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">"</span></a>[ 'rel' x y | E ]" := (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#SimplRel"><span class="id" title="definition">SimplRel</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <span class="id" title="var">E</span>%<span class="id" title="var">B</span>)) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
<span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>, <span class="id" title="var">format</span> "'[hv' [ 'rel' x y | '/ ' E ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">"</span></a>[ 'rel' x y : T | E ]" := (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#SimplRel"><span class="id" title="definition">SimplRel</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <span class="id" title="var">T</span> ⇒ <span class="id" title="var">E</span>%<span class="id" title="var">B</span>)) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
<span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">fun_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">"</span></a>[ 'rel' x y 'in' A & B | E ]" :=<br/>
<a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <span class="id" title="var">A</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <span class="id" title="var">B</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <span class="id" title="var">E</span><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">]</span></a> (<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="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>,<br/>
<span class="id" title="var">format</span> "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">"</span></a>[ 'rel' x y 'in' A & B ]" := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <span class="id" title="var">A</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <span class="id" title="var">B</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">]</span></a><br/>
(<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="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>,<br/>
<span class="id" title="var">format</span> "'[hv' [ 'rel' x y 'in' A & B ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="66e9b5543ed85187fbf7ebcaedd62614"><span class="id" title="notation">"</span></a>[ 'rel' x y 'in' A | E ]" := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">in</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">&</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">|</span></a> <span class="id" title="var">E</span><a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">]</span></a><br/>
(<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="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>,<br/>
<span class="id" title="var">format</span> "'[hv' [ 'rel' x y 'in' A | '/ ' E ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="ec5017d807eee89c28338ba21727b646"><span class="id" title="notation">"</span></a>[ 'rel' x y 'in' A ]" := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">in</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">&</span></a> <span class="id" title="var">A</span><a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">]</span></a> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
<span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>, <span class="id" title="var">format</span> "'[hv' [ 'rel' x y 'in' A ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a name="xrelpre"><span class="id" title="abbreviation">xrelpre</span></a> := (<span class="id" title="keyword">fun</span> <span class="id" title="var">f</span> (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <a class="idref" href="mathcomp.ssreflect.ssrbool.html#r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#y"><span class="id" title="variable">y</span></a>)).<br/>
<span class="id" title="keyword">Definition</span> <a name="relpre"><span class="id" title="definition">relpre</span></a> {<span class="id" title="var">T</span> <span class="id" title="var">rT</span>} (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.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.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#rT"><span class="id" title="variable">rT</span></a>) :=<br/>
<a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#y"><span class="id" title="variable">y</span></a>)<a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">]</span></a>.<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>
|
