diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.ssrbool.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.ssrbool.html | 87 |
1 files changed, 0 insertions, 87 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.ssrbool.html b/docs/htmldoc/mathcomp.ssreflect.ssrbool.html deleted file mode 100644 index baaddd6..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.ssrbool.html +++ /dev/null @@ -1,87 +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.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>
\ No newline at end of file |