diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.choice.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.choice.html | 778 |
1 files changed, 0 insertions, 778 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.choice.html b/docs/htmldoc/mathcomp.ssreflect.choice.html deleted file mode 100644 index 24fce76..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.choice.html +++ /dev/null @@ -1,778 +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.choice</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.ssreflect.choice</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"> - This file contains the definitions of: - choiceType == interface for types with a choice operator. - countType == interface for countable types (implies choiceType). - subCountType == interface for types that are both subType and countType. - xchoose exP == a standard x such that P x, given exP : exists x : T, P x - when T is a choiceType. The choice depends only on the - extent of P (in particular, it is independent of exP). - choose P x0 == if P x0, a standard x such that P x. - pickle x == a nat encoding the value x : T, where T is a countType. - unpickle n == a partial inverse to pickle: unpickle (pickle x) = Some x - pickle_inv n == a sharp partial inverse to pickle pickle_inv n = Some x - if and only if pickle x = n. - choiceMixin T == type of choice mixins; the exact contents is - documented below in the Choice submodule. - ChoiceType T m == the packed choiceType class for T and mixin m. - [choiceType of T for cT] == clone for T of the choiceType cT. - [choiceType of T] == clone for T of the choiceType inferred for T. - CountType T m == the packed countType class for T and mixin m. - [countType of T for cT] == clone for T of the countType cT. - [count Type of T] == clone for T of the countType inferred for T. - [choiceMixin of T by <: ] == Choice mixin for T when T has a subType p - structure with p : pred cT and cT has a Choice - structure; the corresponding structure is Canonical. - [countMixin of T by <: ] == Count mixin for a subType T of a countType. - PcanChoiceMixin fK == Choice mixin for T, given f : T -> cT where cT has - a Choice structure, a left inverse partial function - g and fK : pcancel f g. - CanChoiceMixin fK == Choice mixin for T, given f : T -> cT, g and - fK : cancel f g. - PcanCountMixin fK == Count mixin for T, given f : T -> cT where cT has - a Countable structure, a left inverse partial - function g and fK : pcancel f g. - CanCountMixin fK == Count mixin for T, given f : T -> cT, g and - fK : cancel f g. - GenTree.tree T == generic n-ary tree type with nat-labeled nodes and - T-labeled leaves, for example GenTree.Leaf (x : T), - GenTree.Node 5 [:: t; t' ]. GenTree.tree is equipped - with canonical eqType, choiceType, and countType - instances, and so simple datatypes can be similarly - equipped by encoding into GenTree.tree and using - the mixins above. - CodeSeq.code == bijection from seq nat to nat. - CodeSeq.decode == bijection inverse to CodeSeq.code. - In addition to the lemmas relevant to these definitions, this file also - contains definitions of a Canonical choiceType and countType instances for - all basic datatypes (e.g., nat, bool, subTypes, pairs, sums, etc.). -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -</div> - -<div class="doc"> - Technical definitions about coding and decoding of nat sequences, which - are used below to define various Canonical instances of the choice and - countable interfaces. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Module</span> <a name="CodeSeq"><span class="id" title="module">CodeSeq</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Goedel-style one-to-one encoding of seq nat into nat. - The code for [:: n1; ...; nk] has binary representation - 1 0 ... 0 1 ... 1 0 ... 0 1 0 ... 0 - <-----> <-----> <-----> - nk 0s n2 0s n1 0s -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="CodeSeq.code"><span class="id" title="definition">code</span></a> := <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> ⇒ 2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bff172cdafaf4b86cefb300b16285e42"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>) 0.<br/> - -<br/> -<span class="id" title="keyword">Fixpoint</span> <a name="CodeSeq.decode_rec"><span class="id" title="definition">decode_rec</span></a> (<span class="id" title="var">v</span> <span class="id" title="var">q</span> <span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) {<span class="id" title="keyword">struct</span> <span class="id" title="var">q</span>} :=<br/> - <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#q"><span class="id" title="variable">q</span></a>, <a class="idref" href="mathcomp.ssreflect.choice.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">with</span><br/> - | 0, <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">[::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">]</span></a><br/> - | <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>, 0 ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">rec</span></a> 0<a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">]</span></a><br/> - | <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>, 1 ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">rec</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">]</span></a><br/> - | <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>, <span class="id" title="var">r'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">.+2</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">rec</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">,</span></a> <span class="id" title="var">r'</span><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">]</span></a><br/> - <span class="id" title="keyword">end</span> <span class="id" title="keyword">where</span> <a name="9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">"</span></a>[ 'rec' v , q , r ]" := (<a class="idref" href="mathcomp.ssreflect.choice.html#decode_rec"><span class="id" title="definition">decode_rec</span></a> <span class="id" title="var">v</span> <span class="id" title="var">q</span> <span class="id" title="var">r</span>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="CodeSeq.decode"><span class="id" title="definition">decode</span></a> <span class="id" title="var">n</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> 0 <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">rec</span></a> 0<a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="CodeSeq.decodeK"><span class="id" title="lemma">decodeK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.decode"><span class="id" title="definition">decode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.code"><span class="id" title="definition">code</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="CodeSeq.codeK"><span class="id" title="lemma">codeK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.code"><span class="id" title="definition">code</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.decode"><span class="id" title="definition">decode</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="CodeSeq.ltn_code"><span class="id" title="lemma">ltn_code</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">j</span> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.code"><span class="id" title="definition">code</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="CodeSeq.gtn_decode"><span class="id" title="lemma">gtn_decode</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrnat.html#ltn"><span class="id" title="definition">ltn</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#d89396f990d6b54d736cfe259e498cf4"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.decode"><span class="id" title="definition">decode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>).<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq"><span class="id" title="module">CodeSeq</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="OtherEncodings"><span class="id" title="section">OtherEncodings</span></a>.<br/> -</div> - -<div class="doc"> - Miscellaneous encodings: option T -c-> seq T, T1 * T2 -c-> {i : T1 & T2} - T1 + T2 -c-> option T1 * option T2, unit -c-> bool; bool -c-> nat is - already covered in ssrnat by the nat_of_bool coercion, the odd predicate, - and their "cancellation" lemma oddb. We use these encodings to propagate - canonical structures through these type constructors so that ultimately - all Choice and Countable instanced derive from nat and the seq and sigT - constructors. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Variables</span> <a name="OtherEncodings.T"><span class="id" title="variable">T</span></a> <a name="OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a name="OtherEncodings.T2"><span class="id" title="variable">T2</span></a> : <span class="id" title="keyword">Type</span>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="seq_of_opt"><span class="id" title="definition">seq_of_opt</span></a> := @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#oapp"><span class="id" title="abbreviation">oapp</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T"><span class="id" title="variable">T</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.seq.html#nseq"><span class="id" title="definition">nseq</span></a> 1) <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</span></a>.<br/> -<span class="id" title="keyword">Lemma</span> <a name="seq_of_optK"><span class="id" title="lemma">seq_of_optK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#seq_of_opt"><span class="id" title="definition">seq_of_opt</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#ohead"><span class="id" title="definition">ohead</span></a>. <br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tag_of_pair"><span class="id" title="definition">tag_of_pair</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) := @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#Tagged"><span class="id" title="definition">Tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="pair_of_tag"><span class="id" title="definition">pair_of_tag</span></a> (<span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}</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.ssrfun.html#tag"><span class="id" title="definition">tag</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#u"><span class="id" title="variable">u</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.ssrfun.html#tagged"><span class="id" title="definition">tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#u"><span class="id" title="variable">u</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/> -<span class="id" title="keyword">Lemma</span> <a name="tag_of_pairK"><span class="id" title="lemma">tag_of_pairK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tag_of_pair"><span class="id" title="definition">tag_of_pair</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pair_of_tag"><span class="id" title="definition">pair_of_tag</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="pair_of_tagK"><span class="id" title="lemma">pair_of_tagK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pair_of_tag"><span class="id" title="definition">pair_of_tag</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tag_of_pair"><span class="id" title="definition">tag_of_pair</span></a>. <br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="opair_of_sum"><span class="id" title="definition">opair_of_sum</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) :=<br/> - <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">x</span> ⇒ <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.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">x</span><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.Init.Datatypes.html#None"><span class="id" title="constructor">None</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.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <span class="id" title="var">y</span> ⇒ <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.Init.Datatypes.html#None"><span class="id" title="constructor">None</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.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">y</span><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> <span class="id" title="keyword">end</span>.<br/> -<span class="id" title="keyword">Definition</span> <a name="sum_of_opair"><span class="id" title="definition">sum_of_opair</span></a> <span class="id" title="var">p</span> :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#oapp"><span class="id" title="abbreviation">oapp</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#some"><span class="id" title="abbreviation">some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">o</span></a> @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#omap"><span class="id" title="abbreviation">omap</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a>.<br/> -<span class="id" title="keyword">Lemma</span> <a name="opair_of_sumK"><span class="id" title="lemma">opair_of_sumK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#opair_of_sum"><span class="id" title="definition">opair_of_sum</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sum_of_opair"><span class="id" title="definition">sum_of_opair</span></a>. <br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="bool_of_unitK"><span class="id" title="lemma">bool_of_unitK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <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>) (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</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/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings"><span class="id" title="section">OtherEncodings</span></a>.<br/> - -<br/> - -<br/> -</div> - -<div class="doc"> - Generic variable-arity tree type, providing an encoding target for - miscellaneous user datatypes. The GenTree.tree type can be combined with - a sigT type to model multi-sorted concrete datatypes. -</div> -<div class="code"> -<span class="id" title="keyword">Module</span> <a name="GenTree"><span class="id" title="module">GenTree</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="GenTree.Def"><span class="id" title="section">Def</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="GenTree.Def.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>.<br/> - -<br/> -<span class="id" title="keyword">Inductive</span> <a name="GenTree.tree"><span class="id" title="inductive">tree</span></a> := <a name="GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Def.T"><span class="id" title="variable">T</span></a> | <a name="GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> & <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tree"><span class="id" title="inductive">tree</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="GenTree.tree_rect"><span class="id" title="definition">tree_rect</span></a> <span class="id" title="var">K</span> <span class="id" title="var">IH_leaf</span> <span class="id" title="var">IH_node</span> :=<br/> - <span class="id" title="keyword">fix</span> <span class="id" title="var">loop</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> := <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/> - | <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#IH_leaf"><span class="id" title="variable">IH_leaf</span></a> <span class="id" title="var">x</span><br/> - | <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f0</span> ⇒<br/> - <span class="id" title="keyword">let</span> <span class="id" title="keyword">fix</span> <span class="id" title="var">iter_pair</span> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">t</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#prod"><span class="id" title="inductive">prod</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> :=<br/> - <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <span class="id" title="var">f'</span> <span class="id" title="keyword">then</span> <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.choice.html#loop"><span class="id" title="variable">loop</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#iter_pair"><span class="id" title="variable">iter_pair</span></a> <span class="id" title="var">f'</span><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> <span class="id" title="keyword">else</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="tactic">in</span><br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#IH_node"><span class="id" title="variable">IH_node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f0</span> (<a class="idref" href="mathcomp.ssreflect.choice.html#iter_pair"><span class="id" title="variable">iter_pair</span></a> <span class="id" title="var">f0</span>)<br/> - <span class="id" title="keyword">end</span>.<br/> -<span class="id" title="keyword">Definition</span> <a name="GenTree.tree_rec"><span class="id" title="definition">tree_rec</span></a> (<span class="id" title="var">K</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.tree"><span class="id" title="inductive">tree</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> <span class="id" title="keyword">Set</span>) := @<a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.tree_rect"><span class="id" title="definition">tree_rect</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="GenTree.tree_ind"><span class="id" title="definition">tree_ind</span></a> <span class="id" title="var">K</span> <span class="id" title="var">IH_leaf</span> <span class="id" title="var">IH_node</span> :=<br/> - <span class="id" title="keyword">fix</span> <span class="id" title="var">loop</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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.ssreflect.html#17ff6c89d595412214a9dd9e39474c36"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#17ff6c89d595412214a9dd9e39474c36"><span class="id" title="notation">Prop</span></a> := <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/> - | <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#IH_leaf"><span class="id" title="variable">IH_leaf</span></a> <span class="id" title="var">x</span><br/> - | <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f0</span> ⇒<br/> - <span class="id" title="keyword">let</span> <span class="id" title="keyword">fix</span> <span class="id" title="var">iter_conj</span> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">t</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#and"><span class="id" title="inductive">and</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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#True"><span class="id" title="inductive">True</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> :=<br/> - <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <span class="id" title="var">f'</span> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#conj"><span class="id" title="constructor">conj</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#loop"><span class="id" title="variable">loop</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#iter_conj"><span class="id" title="variable">iter_conj</span></a> <span class="id" title="var">f'</span>) <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#I"><span class="id" title="constructor">Logic.I</span></a><br/> - <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#IH_node"><span class="id" title="variable">IH_node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f0</span> (<a class="idref" href="mathcomp.ssreflect.choice.html#iter_conj"><span class="id" title="variable">iter_conj</span></a> <span class="id" title="var">f0</span>)<br/> - <span class="id" title="keyword">end</span>.<br/> - -<br/> -<span class="id" title="keyword">Fixpoint</span> <a name="GenTree.encode"><span class="id" title="definition">encode</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Def.T"><span class="id" title="variable">T</span></a>) :=<br/> - <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/> - | <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">[::</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <span class="id" title="var">_</span> <span class="id" title="var">x</span><a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">]</span></a><br/> - | <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">_</span> <span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#rcons"><span class="id" title="definition">rcons</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#flatten"><span class="id" title="definition">flatten</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#encode"><span class="id" title="definition">encode</span></a> <span class="id" title="var">f</span>)) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">_</span> 0)<br/> - <span class="id" title="keyword">end</span>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="GenTree.decode_step"><span class="id" title="definition">decode_step</span></a> <span class="id" title="var">c</span> <span class="id" title="var">fs</span> := <br/> - <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">with</span><br/> - | <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <span class="id" title="var">x</span> ⇒ <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.choice.html#GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</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.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</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/> - | <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> 0 ⇒ <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.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</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.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</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/> - | <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</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.choice.html#GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="var">n</span> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#head"><span class="id" title="definition">head</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</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.seq.html#behead"><span class="id" title="definition">behead</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</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/> - <span class="id" title="keyword">end</span>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="GenTree.decode"><span class="id" title="definition">decode</span></a> <span class="id" title="var">c</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#ohead"><span class="id" title="definition">ohead</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.decode_step"><span class="id" title="definition">decode_step</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.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</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.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</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.choice.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">).1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="GenTree.codeK"><span class="id" title="lemma">codeK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.encode"><span class="id" title="definition">encode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.decode"><span class="id" title="definition">decode</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Def"><span class="id" title="section">Def</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree"><span class="id" title="module">GenTree</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tree_eqMixin"><span class="id" title="definition">tree_eqMixin</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) := <a class="idref" href="mathcomp.ssreflect.eqtype.html#PcanEqMixin"><span class="id" title="definition">PcanEqMixin</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#codeK"><span class="id" title="lemma">GenTree.codeK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tree_eqType</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#tree"><span class="id" title="inductive">GenTree.tree</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#tree_eqMixin"><span class="id" title="definition">tree_eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -</div> - -<div class="doc"> - Structures for Types with a choice function, and for Types with countably - many elements. The two concepts are closely linked: we indeed make - Countable a subclass of Choice, as countable choice is valid in CiC. This - apparent redundancy is needed to ensure the consistency of the Canonical - inference, as the canonical Choice for a given type may differ from the - countable choice for its canonical Countable structure, e.g., for options. - The Choice interface exposes two choice functions; for T : choiceType - and P : pred T, we provide: - xchoose : (exists x, P x) -> T - choose : pred T -> T -> T - While P (xchoose exP) will always hold, P (choose P x0) will be true if - and only if P x0 holds. Both xchoose and choose are extensional in P and - do not depend on the witness exP or x0 (provided P x0 holds). Note that - xchoose is slightly more powerful, but less convenient to use. - However, neither choose nor xchoose are composable: it would not be - be possible to extend the Choice structure to arbitrary pairs using only - these functions, for instance. Internally, the interfaces provides a - subtly stronger operation, Choice.InternalTheory.find, which performs a - limited search using an integer parameter only rather than a full value as - [x]choose does. This is not a restriction in a constructive theory, where - all types are concrete and hence countable. In the case of an axiomatic - theory, such as that of the Coq reals library, postulating a suitable - axiom of choice suppresses the need for guidance. Nevertheless this - operation is just what is needed to make the Choice interface compose. - The Countable interface provides three functions; for T : countType we - get pickle : T -> nat, and unpickle, pickle_inv : nat -> option T. - The functions provide an effective embedding of T in nat: unpickle is a - left inverse to pickle, which satisfies pcancel pickle unpickle, i.e., - unpickle \o pickle =1 some; pickle_inv is a more precise inverse for which - we also have ocancel pickle_inv pickle. Both unpickle and pickle need to - be partial functions to allow for possibly empty types such as {x | P x}. - The names of these functions underline the correspondence with the - notion of "Serializable" types in programming languages. - Finally, we need to provide a join class to let type inference unify - subType and countType class constraints, e.g., for a countable subType of - an uncountable choiceType (the issue does not arise earlier with eqType or - choiceType because in practice the base type of an Equality/Choice subType - is always an Equality/Choice Type). -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Module</span> <a name="Choice"><span class="id" title="module">Choice</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Choice.ClassDef"><span class="id" title="section">ClassDef</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Record</span> <a name="Choice.mixin_of"><span class="id" title="record">mixin_of</span></a> <span class="id" title="var">T</span> := <a name="Choice.Mixin"><span class="id" title="constructor">Mixin</span></a> {<br/> - <a name="Choice.find"><span class="id" title="projection">find</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.choice.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.Datatypes.html#nat"><span class="id" title="inductive">nat</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#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>;<br/> - <span class="id" title="var">_</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> <span class="id" title="var">n</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.choice.html#find"><span class="id" title="method">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</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.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a>;<br/> - <span class="id" title="var">_</span> : <span class="id" title="keyword">∀</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.choice.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#a883bdd010993579f99d60b3775bcf54"><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.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</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.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#find"><span class="id" title="method">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>;<br/> - <span class="id" title="var">_</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</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.choice.html#T"><span class="id" title="variable">T</span></a>, <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</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.choice.html#find"><span class="id" title="method">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#find"><span class="id" title="method">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a><br/> -}.<br/> - -<br/> -<span class="id" title="keyword">Record</span> <a name="Choice.class_of"><span class="id" title="record">class_of</span></a> <span class="id" title="var">T</span> := <a name="Choice.Class"><span class="id" title="constructor">Class</span></a> {<a name="Choice.base"><span class="id" title="projection">base</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.class_of"><span class="id" title="abbreviation">Equality.class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>; <a name="Choice.mixin"><span class="id" title="projection">mixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.mixin_of"><span class="id" title="record">mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>}.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="Choice.type"><span class="id" title="record">type</span></a> := <a name="Choice.Pack"><span class="id" title="constructor">Pack</span></a> {<a name="Choice.sort"><span class="id" title="projection">sort</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sort"><span class="id" title="method">sort</span></a>}.<br/> -<span class="id" title="keyword">Variables</span> (<a name="Choice.ClassDef.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>) (<a name="Choice.ClassDef.cT"><span class="id" title="variable">cT</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.type"><span class="id" title="record">type</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="Choice.class"><span class="id" title="definition">class</span></a> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">c</span> <span class="id" title="keyword">as</span> <span class="id" title="var">cT'</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.cT"><span class="id" title="variable">cT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#cT'"><span class="id" title="variable">cT'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">c</span>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Choice.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">c</span> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class"><span class="id" title="definition">class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a> := @<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a>.<br/> -<span class="id" title="keyword">Let</span> <a name="Choice.ClassDef.xT"><span class="id" title="variable">xT</span></a> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Pack</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.cT"><span class="id" title="variable">cT</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">T</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Choice.xclass"><span class="id" title="abbreviation">xclass</span></a> := (<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class"><span class="id" title="definition">class</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.choice.html#Choice.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.xT"><span class="id" title="variable">xT</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Choice.pack"><span class="id" title="definition">pack</span></a> <span class="id" title="var">m</span> :=<br/> - <span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> <span class="id" title="var">bT</span> & <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.class"><span class="id" title="definition">Equality.class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bT"><span class="id" title="variable">bT</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Pack</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Class"><span class="id" title="constructor">Class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>).<br/> - -<br/> -</div> - -<div class="doc"> - Inheritance -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="Choice.eqType"><span class="id" title="definition">eqType</span></a> := @<a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Pack"><span class="id" title="constructor">Equality.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.xclass"><span class="id" title="abbreviation">xclass</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef"><span class="id" title="section">ClassDef</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Import</span> <a name="Choice.Exports"><span class="id" title="module">Exports</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">base</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">Equality.class_of</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">sort</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">Sortclass</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">Equality.type</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqType</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.type"><span class="id" title="record">type</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Choice.Exports.choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.mixin_of"><span class="id" title="record">mixin_of</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.pack"><span class="id" title="definition">pack</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>).<br/> -<span class="id" title="keyword">Notation</span> <a name="5aecd629a84e4074bfe0a7de23c55d82"><span class="id" title="notation">"</span></a>[ 'choiceType' 'of' T 'for' cT ]" := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">T</span> <span class="id" title="var">cT</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#idfun"><span class="id" title="abbreviation">idfun</span></a>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'choiceType' 'of' T 'for' cT ]") : <span class="id" title="var">form_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="6cecb3ca492751e55998eec154506328"><span class="id" title="notation">"</span></a>[ 'choiceType' 'of' T ]" := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'choiceType' 'of' T ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports"><span class="id" title="module">Exports</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="Choice.InternalTheory"><span class="id" title="module">InternalTheory</span></a>.<br/> -<span class="id" title="keyword">Section</span> <a name="Choice.InternalTheory.InternalTheory"><span class="id" title="section">InternalTheory</span></a>.<br/> -</div> - -<div class="doc"> - Inner choice function. -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.find"><span class="id" title="projection">find</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.mixin"><span class="id" title="projection">mixin</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class"><span class="id" title="definition">class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Choice.InternalTheory.InternalTheory.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</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.choice.html#Choice.InternalTheory.InternalTheory.T"><span class="id" title="variable">T</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Choice.InternalTheory.correct"><span class="id" title="lemma">correct</span></a> <span class="id" title="var">P</span> <span class="id" title="var">n</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</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.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Choice.InternalTheory.complete"><span class="id" title="lemma">complete</span></a> <span class="id" title="var">P</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><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.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</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.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#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Choice.InternalTheory.extensional"><span class="id" title="lemma">extensional</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> : <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</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.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="Choice.InternalTheory.xchoose_subproof"><span class="id" title="lemma">xchoose_subproof</span></a> <span class="id" title="var">P</span> <span class="id" title="var">exP</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrnat.html#ex_minn"><span class="id" title="definition">ex_minn</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.complete"><span class="id" title="lemma">complete</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exP"><span class="id" title="variable">exP</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.InternalTheory"><span class="id" title="section">InternalTheory</span></a>.<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory"><span class="id" title="module">InternalTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice"><span class="id" title="module">Choice</span></a>.<br/> -<span class="id" title="keyword">Export</span> <span class="id" title="var">Choice.Exports</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ChoiceTheory"><span class="id" title="section">ChoiceTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>.<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">Choice.InternalTheory</span> <span class="id" title="var">CodeSeq</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ChoiceTheory.OneType"><span class="id" title="section">OneType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</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.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="xchoose"><span class="id" title="definition">xchoose</span></a> <span class="id" title="var">P</span> <span class="id" title="var">exP</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#sval"><span class="id" title="abbreviation">sval</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#xchoose_subproof"><span class="id" title="lemma">xchoose_subproof</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exP"><span class="id" title="variable">exP</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="xchooseP"><span class="id" title="lemma">xchooseP</span></a> <span class="id" title="var">P</span> <span class="id" title="var">exP</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#xchoose"><span class="id" title="definition">xchoose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exP"><span class="id" title="variable">exP</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eq_xchoose"><span class="id" title="lemma">eq_xchoose</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> <span class="id" title="var">exP</span> <span class="id" title="var">exQ</span> : <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</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.choice.html#xchoose"><span class="id" title="definition">xchoose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exP"><span class="id" title="variable">exP</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> @<a class="idref" href="mathcomp.ssreflect.choice.html#xchoose"><span class="id" title="definition">xchoose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exQ"><span class="id" title="variable">exQ</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sigW"><span class="id" title="lemma">sigW</span></a> <span class="id" title="var">P</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><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.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sig2W"><span class="id" title="lemma">sig2W</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</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.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sig_eqW"><span class="id" title="lemma">sig_eqW</span></a> (<span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<span class="id" title="var">lhs</span> <span class="id" title="var">rhs</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.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.choice.html#vT"><span class="id" title="variable">vT</span></a>) :<br/> - <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#a883bdd010993579f99d60b3775bcf54"><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.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#lhs"><span class="id" title="variable">lhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#rhs"><span class="id" title="variable">rhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#lhs"><span class="id" title="variable">lhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#rhs"><span class="id" title="variable">rhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sig2_eqW"><span class="id" title="lemma">sig2_eqW</span></a> (<span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<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.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">lhs</span> <span class="id" title="var">rhs</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.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.choice.html#vT"><span class="id" title="variable">vT</span></a>) :<br/> - <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#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#lhs"><span class="id" title="variable">lhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#rhs"><span class="id" title="variable">rhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</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.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#lhs"><span class="id" title="variable">lhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#rhs"><span class="id" title="variable">rhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="choose"><span class="id" title="definition">choose</span></a> <span class="id" title="var">P</span> <span class="id" title="var">x0</span> :=<br/> - <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#insub"><span class="id" title="definition">insub</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</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.eqtype.html#ffdab75dfbdeb52617eb82d58d4bcb84"><span class="id" title="notation">{?</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#ffdab75dfbdeb52617eb82d58d4bcb84"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#ffdab75dfbdeb52617eb82d58d4bcb84"><span class="id" title="notation">}</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#exist"><span class="id" title="constructor">exist</span></a> <span class="id" title="var">x</span> <span class="id" title="var">Px</span>) <span class="id" title="keyword">then</span><br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#xchoose"><span class="id" title="definition">xchoose</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ex_intro"><span class="id" title="constructor">ex_intro</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#20b75710d0541e9ffd06f8e723fd3daf"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#20b75710d0541e9ffd06f8e723fd3daf"><span class="id" title="notation">eta</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#20b75710d0541e9ffd06f8e723fd3daf"><span class="id" title="notation">]</span></a> <span class="id" title="var">x</span> <span class="id" title="var">Px</span>)<br/> - <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="chooseP"><span class="id" title="lemma">chooseP</span></a> <span class="id" title="var">P</span> <span class="id" title="var">x0</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</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.choice.html#P"><span class="id" title="variable">P</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="choose_id"><span class="id" title="lemma">choose_id</span></a> <span class="id" title="var">P</span> <span class="id" title="var">x0</span> <span class="id" title="var">y0</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</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.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#y0"><span class="id" title="variable">y0</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.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#y0"><span class="id" title="variable">y0</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eq_choose"><span class="id" title="lemma">eq_choose</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> : <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</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.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.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.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ChoiceTheory.OneType.CanChoice"><span class="id" title="section">CanChoice</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="ChoiceTheory.OneType.CanChoice.sT"><span class="id" title="variable">sT</span></a> : <span class="id" title="keyword">Type</span>) (<a name="ChoiceTheory.OneType.CanChoice.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</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.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> <span class="id" title="var">f'</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.CanChoice.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</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.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.CanChoice.sT"><span class="id" title="variable">sT</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> <span class="id" title="var">f'</span> (<span class="id" title="var">fK</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.CanChoice.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#can_pcan"><span class="id" title="lemma">can_pcan</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fK"><span class="id" title="variable">fK</span></a>).<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.CanChoice"><span class="id" title="section">CanChoice</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ChoiceTheory.OneType.SubChoice"><span class="id" title="section">SubChoice</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="ChoiceTheory.OneType.SubChoice.P"><span class="id" title="variable">P</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.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>) (<a name="ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#subType"><span class="id" title="record">subType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="sub_choiceMixin"><span class="id" title="definition">sub_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.eqtype.html#valK"><span class="id" title="lemma">valK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="sub_choiceClass"><span class="id" title="definition">sub_choiceClass</span></a> := @<a class="idref" href="mathcomp.ssreflect.choice.html#Class"><span class="id" title="constructor">Choice.Class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#sub_eqMixin"><span class="id" title="definition">sub_eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#sub_choiceMixin"><span class="id" title="definition">sub_choiceMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sub_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Pack"><span class="id" title="constructor">Choice.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sub_choiceClass"><span class="id" title="definition">sub_choiceClass</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice"><span class="id" title="section">SubChoice</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="seq_choiceMixin"><span class="id" title="lemma">seq_choiceMixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">seq_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#seq_choiceMixin"><span class="id" title="lemma">seq_choiceMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType"><span class="id" title="section">OneType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ChoiceTheory.TagChoice"><span class="id" title="section">TagChoice</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="ChoiceTheory.TagChoice.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<a name="ChoiceTheory.TagChoice.T_"><span class="id" title="variable">T_</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#I"><span class="id" title="variable">I</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.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="tagged_choiceMixin"><span class="id" title="lemma">tagged_choiceMixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice.I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice.T_"><span class="id" title="variable">T_</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tagged_choiceType</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice.I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice.T_"><span class="id" title="variable">T_</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tagged_choiceMixin"><span class="id" title="lemma">tagged_choiceMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice"><span class="id" title="section">TagChoice</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="nat_choiceMixin"><span class="id" title="lemma">nat_choiceMixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">nat_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#nat_choiceMixin"><span class="id" title="lemma">nat_choiceMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="bool_choiceMixin"><span class="id" title="definition">bool_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#oddb"><span class="id" title="lemma">oddb</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bool_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</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 class="idref" href="mathcomp.ssreflect.choice.html#bool_choiceMixin"><span class="id" title="definition">bool_choiceMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bitseq_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#bitseq"><span class="id" title="definition">bitseq</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="unit_choiceMixin"><span class="id" title="definition">unit_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bool_of_unitK"><span class="id" title="lemma">bool_of_unitK</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unit_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</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.choice.html#unit_choiceMixin"><span class="id" title="definition">unit_choiceMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="option_choiceMixin"><span class="id" title="definition">option_choiceMixin</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#seq_of_optK"><span class="id" title="lemma">seq_of_optK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">option_choiceType</span> <span class="id" title="var">T</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#option_choiceMixin"><span class="id" title="definition">option_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="sig_choiceMixin"><span class="id" title="definition">sig_choiceMixin</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.choice.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a> :=<br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#sub_choiceMixin"><span class="id" title="definition">sub_choiceMixin</span></a> <span class="id" title="var">_</span>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sig_choiceType</span> <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.choice.html#T"><span class="id" title="variable">T</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#sig_choiceMixin"><span class="id" title="definition">sig_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="prod_choiceMixin"><span class="id" title="definition">prod_choiceMixin</span></a> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#tag_of_pairK"><span class="id" title="lemma">tag_of_pairK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">prod_choiceType</span> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#prod_choiceMixin"><span class="id" title="definition">prod_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="sum_choiceMixin"><span class="id" title="definition">sum_choiceMixin</span></a> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#opair_of_sumK"><span class="id" title="lemma">opair_of_sumK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sum_choiceType</span> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#sum_choiceMixin"><span class="id" title="definition">sum_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tree_choiceMixin"><span class="id" title="definition">tree_choiceMixin</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#codeK"><span class="id" title="lemma">GenTree.codeK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tree_choiceType</span> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#tree"><span class="id" title="inductive">GenTree.tree</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#tree_choiceMixin"><span class="id" title="definition">tree_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory"><span class="id" title="section">ChoiceTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">"</span></a>[ 'choiceMixin' 'of' T 'by' <: ]" :=<br/> - (<a class="idref" href="mathcomp.ssreflect.choice.html#sub_choiceMixin"><span class="id" title="definition">sub_choiceMixin</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> <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <span class="id" title="var">T</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'choiceMixin' 'of' T 'by' <: ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="Countable"><span class="id" title="module">Countable</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Record</span> <a name="Countable.mixin_of"><span class="id" title="record">mixin_of</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a name="Countable.Mixin"><span class="id" title="constructor">Mixin</span></a> {<br/> - <a name="Countable.pickle"><span class="id" title="projection">pickle</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.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.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>;<br/> - <a name="Countable.unpickle"><span class="id" title="projection">unpickle</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</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#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>;<br/> - <a name="Countable.pickleK"><span class="id" title="projection">pickleK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="method">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="method">unpickle</span></a><br/> -}.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Countable.EqMixin"><span class="id" title="definition">EqMixin</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#PcanEqMixin"><span class="id" title="definition">PcanEqMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.pickleK"><span class="id" title="projection">pickleK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="Countable.ChoiceMixin"><span class="id" title="definition">ChoiceMixin</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.pickleK"><span class="id" title="projection">pickleK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Countable.ClassDef"><span class="id" title="section">ClassDef</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Record</span> <a name="Countable.class_of"><span class="id" title="record">class_of</span></a> <span class="id" title="var">T</span> := <a name="Countable.Class"><span class="id" title="constructor">Class</span></a> { <a name="Countable.base"><span class="id" title="projection">base</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class_of"><span class="id" title="record">Choice.class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>; <a name="Countable.mixin"><span class="id" title="projection">mixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin_of"><span class="id" title="record">mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a> }.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="Countable.type"><span class="id" title="record">type</span></a> : <span class="id" title="keyword">Type</span> := <a name="Countable.Pack"><span class="id" title="constructor">Pack</span></a> {<a name="Countable.sort"><span class="id" title="projection">sort</span></a> : <span class="id" title="keyword">Type</span>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sort"><span class="id" title="method">sort</span></a>}.<br/> -<span class="id" title="keyword">Variables</span> (<a name="Countable.ClassDef.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>) (<a name="Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.type"><span class="id" title="record">type</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="Countable.class"><span class="id" title="definition">class</span></a> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Pack"><span class="id" title="constructor">Pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">c</span> <span class="id" title="keyword">as</span> <span class="id" title="var">cT'</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#cT'"><span class="id" title="variable">cT'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">c</span>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Countable.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">c</span> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class"><span class="id" title="definition">class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a> := @<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Pack"><span class="id" title="constructor">Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a>.<br/> -<span class="id" title="keyword">Let</span> <a name="Countable.ClassDef.xT"><span class="id" title="variable">xT</span></a> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Pack"><span class="id" title="constructor">Pack</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">T</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Countable.xclass"><span class="id" title="abbreviation">xclass</span></a> := (<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class"><span class="id" title="definition">class</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.choice.html#Countable.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.xT"><span class="id" title="variable">xT</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Countable.pack"><span class="id" title="definition">pack</span></a> <span class="id" title="var">m</span> :=<br/> - <span class="id" title="keyword">fun</span> <span class="id" title="var">bT</span> <span class="id" title="var">b</span> & <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class"><span class="id" title="definition">Choice.class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bT"><span class="id" title="variable">bT</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Pack"><span class="id" title="constructor">Pack</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Class"><span class="id" title="constructor">Class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Countable.eqType"><span class="id" title="definition">eqType</span></a> := @<a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Pack"><span class="id" title="constructor">Equality.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.xclass"><span class="id" title="abbreviation">xclass</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Countable.choiceType"><span class="id" title="definition">choiceType</span></a> := @<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Choice.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.xclass"><span class="id" title="abbreviation">xclass</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef"><span class="id" title="section">ClassDef</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="Countable.Exports"><span class="id" title="module">Exports</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">base</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">Choice.class_of</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">mixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">mixin_of</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">sort</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">Sortclass</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">Equality.type</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqType</span>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">Choice.type</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">choiceType</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.type"><span class="id" title="record">type</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.pack"><span class="id" title="definition">pack</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>).<br/> -<span class="id" title="keyword">Notation</span> <a name="Countable.Exports.CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Mixin"><span class="id" title="constructor">Mixin</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="Countable.Exports.CountChoiceMixin"><span class="id" title="abbreviation">CountChoiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ChoiceMixin"><span class="id" title="definition">ChoiceMixin</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="6b64a8182e19cfcfdb25b3be2b7f0d83"><span class="id" title="notation">"</span></a>[ 'countType' 'of' T 'for' cT ]" := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">T</span> <span class="id" title="var">cT</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#idfun"><span class="id" title="abbreviation">idfun</span></a>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'countType' 'of' T 'for' cT ]") : <span class="id" title="var">form_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">"</span></a>[ 'countType' 'of' T ]" := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'countType' 'of' T ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports"><span class="id" title="module">Exports</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable"><span class="id" title="module">Countable</span></a>.<br/> -<span class="id" title="keyword">Export</span> <span class="id" title="var">Countable.Exports</span>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="unpickle"><span class="id" title="definition">unpickle</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="projection">Countable.unpickle</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#class"><span class="id" title="definition">Countable.class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="pickle"><span class="id" title="definition">pickle</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="projection">Countable.pickle</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#class"><span class="id" title="definition">Countable.class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="CountableTheory"><span class="id" title="section">CountableTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="CountableTheory.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#countType"><span class="id" title="abbreviation">countType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pickleK"><span class="id" title="lemma">pickleK</span></a> : @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="pickle_inv"><span class="id" title="definition">pickle_inv</span></a> <span class="id" title="var">n</span> :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#obind"><span class="id" title="abbreviation">obind</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">else</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pickle_invK"><span class="id" title="lemma">pickle_invK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#ocancel"><span class="id" title="definition">ocancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_inv"><span class="id" title="definition">pickle_inv</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pickleK_inv"><span class="id" title="lemma">pickleK_inv</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_inv"><span class="id" title="definition">pickle_inv</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pcan_pickleK"><span class="id" title="lemma">pcan_pickleK</span></a> <span class="id" title="var">sT</span> <span class="id" title="var">f</span> <span class="id" title="var">f'</span> :<br/> - @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</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.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcomp"><span class="id" title="definition">pcomp</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> <span class="id" title="var">sT</span> <span class="id" title="var">f</span> <span class="id" title="var">f'</span> (<span class="id" title="var">fK</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a>) :=<br/> - @<a class="idref" href="mathcomp.ssreflect.choice.html#CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.choice.html#pcan_pickleK"><span class="id" title="lemma">pcan_pickleK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fK"><span class="id" title="variable">fK</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> <span class="id" title="var">sT</span> <span class="id" title="var">f</span> <span class="id" title="var">f'</span> (<span class="id" title="var">fK</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a>) :=<br/> - @<a class="idref" href="mathcomp.ssreflect.choice.html#PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#can_pcan"><span class="id" title="lemma">can_pcan</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fK"><span class="id" title="variable">fK</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="sub_countMixin"><span class="id" title="definition">sub_countMixin</span></a> <span class="id" title="var">P</span> <span class="id" title="var">sT</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.eqtype.html#valK"><span class="id" title="lemma">valK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="pickle_seq"><span class="id" title="definition">pickle_seq</span></a> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#code"><span class="id" title="definition">CodeSeq.code</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="unpickle_seq"><span class="id" title="definition">unpickle_seq</span></a> <span class="id" title="var">n</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#pmap"><span class="id" title="definition">pmap</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#decode"><span class="id" title="definition">CodeSeq.decode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>)).<br/> -<span class="id" title="keyword">Lemma</span> <a name="pickle_seqK"><span class="id" title="lemma">pickle_seqK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_seq"><span class="id" title="definition">pickle_seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle_seq"><span class="id" title="definition">unpickle_seq</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="seq_countMixin"><span class="id" title="definition">seq_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_seqK"><span class="id" title="lemma">pickle_seqK</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">seq_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#seq_countMixin"><span class="id" title="definition">seq_countMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory"><span class="id" title="section">CountableTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">"</span></a>[ 'countMixin' 'of' T 'by' <: ]" :=<br/> - (<a class="idref" href="mathcomp.ssreflect.choice.html#sub_countMixin"><span class="id" title="definition">sub_countMixin</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> <a class="idref" href="mathcomp.ssreflect.choice.html#mixin_of"><span class="id" title="record">Countable.mixin_of</span></a> <span class="id" title="var">T</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'countMixin' 'of' T 'by' <: ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="SubCountType"><span class="id" title="section">SubCountType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="SubCountType.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<a name="SubCountType.P"><span class="id" title="variable">P</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.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">Countable</span>.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="subCountType"><span class="id" title="record">subCountType</span></a> : <span class="id" title="keyword">Type</span> :=<br/> - <a name="SubCountType"><span class="id" title="constructor">SubCountType</span></a> {<a name="subCount_sort"><span class="id" title="projection">subCount_sort</span></a> :> <a class="idref" href="mathcomp.ssreflect.eqtype.html#subType"><span class="id" title="record">subType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#SubCountType.P"><span class="id" title="variable">P</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#mixin_of"><span class="id" title="record">mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#subCount_sort"><span class="id" title="method">subCount_sort</span></a>}.<br/> - -<br/> -<span class="id" title="keyword">Coercion</span> <span class="id" title="var">sub_countType</span> (<span class="id" title="var">sT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#subCountType"><span class="id" title="record">subCountType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#pack"><span class="id" title="definition">pack</span></a> (<span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#SubCountType"><span class="id" title="constructor">SubCountType</span></a> <span class="id" title="var">_</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.choice.html#mixin_of"><span class="id" title="record">mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">m</span>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sub_countType</span>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="pack_subCountType"><span class="id" title="definition">pack_subCountType</span></a> <span class="id" title="var">U</span> :=<br/> - <span class="id" title="keyword">fun</span> <span class="id" title="var">sT</span> <span class="id" title="var">cT</span> & <a class="idref" href="mathcomp.ssreflect.eqtype.html#sub_sort"><span class="id" title="projection">sub_sort</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sort"><span class="id" title="projection">sort</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#cT"><span class="id" title="variable">cT</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.choice.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#U"><span class="id" title="variable">U</span></a> ⇒<br/> - <span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> <span class="id" title="var">m</span> & <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#Class"><span class="id" title="constructor">Class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#class"><span class="id" title="definition">class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#cT"><span class="id" title="variable">cT</span></a>) ⇒ @<a class="idref" href="mathcomp.ssreflect.choice.html#SubCountType"><span class="id" title="constructor">SubCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#SubCountType"><span class="id" title="section">SubCountType</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This assumes that T has both countType and subType structures. -</div> -<div class="code"> -<span class="id" title="keyword">Notation</span> <a name="9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">"</span></a>[ 'subCountType' 'of' T ]" :=<br/> - (@<a class="idref" href="mathcomp.ssreflect.choice.html#pack_subCountType"><span class="id" title="definition">pack_subCountType</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'subCountType' 'of' T ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="TagCountType"><span class="id" title="section">TagCountType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="TagCountType.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#countType"><span class="id" title="abbreviation">countType</span></a>) (<a name="TagCountType.T_"><span class="id" title="variable">T_</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#I"><span class="id" title="variable">I</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.choice.html#countType"><span class="id" title="abbreviation">countType</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="pickle_tagged"><span class="id" title="definition">pickle_tagged</span></a> (<span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.T_"><span class="id" title="variable">T_</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#code"><span class="id" title="definition">CodeSeq.code</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#9e9281397dab83046645f1b62dbb2487"><span class="id" title="notation">[::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#tag"><span class="id" title="definition">tag</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#u"><span class="id" title="variable">u</span></a>)<a class="idref" href="mathcomp.ssreflect.seq.html#9e9281397dab83046645f1b62dbb2487"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#tagged"><span class="id" title="definition">tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#u"><span class="id" title="variable">u</span></a>)<a class="idref" href="mathcomp.ssreflect.seq.html#9e9281397dab83046645f1b62dbb2487"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="unpickle_tagged"><span class="id" title="definition">unpickle_tagged</span></a> <span class="id" title="var">s</span> :=<br/> - <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.choice.html#decode"><span class="id" title="definition">CodeSeq.decode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="mathcomp.ssreflect.seq.html#9e9281397dab83046645f1b62dbb2487"><span class="id" title="notation">[::</span></a> <span class="id" title="var">ni</span><a class="idref" href="mathcomp.ssreflect.seq.html#9e9281397dab83046645f1b62dbb2487"><span class="id" title="notation">;</span></a> <span class="id" title="var">nx</span><a class="idref" href="mathcomp.ssreflect.seq.html#9e9281397dab83046645f1b62dbb2487"><span class="id" title="notation">]</span></a> <span class="id" title="keyword">then</span><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#obind"><span class="id" title="abbreviation">obind</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">i</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#omap"><span class="id" title="abbreviation">omap</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#Tagged"><span class="id" title="definition">Tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.I"><span class="id" title="variable">I</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.T_"><span class="id" title="variable">T_</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a> <span class="id" title="var">nx</span>)) (<a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a> <span class="id" title="var">ni</span>)<br/> - <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/> -<span class="id" title="keyword">Lemma</span> <a name="pickle_taggedK"><span class="id" title="lemma">pickle_taggedK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_tagged"><span class="id" title="definition">pickle_tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle_tagged"><span class="id" title="definition">unpickle_tagged</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tag_countMixin"><span class="id" title="definition">tag_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_taggedK"><span class="id" title="lemma">pickle_taggedK</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tag_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.T_"><span class="id" title="variable">T_</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tag_countMixin"><span class="id" title="definition">tag_countMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType"><span class="id" title="section">TagCountType</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - The remaining Canonicals for standard datatypes. -</div> -<div class="code"> -<span class="id" title="keyword">Section</span> <a name="CountableDataTypes"><span class="id" title="section">CountableDataTypes</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#countType"><span class="id" title="abbreviation">countType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="nat_pickleK"><span class="id" title="lemma">nat_pickleK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>). <br/> -<span class="id" title="keyword">Definition</span> <a name="nat_countMixin"><span class="id" title="definition">nat_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#nat_pickleK"><span class="id" title="lemma">nat_pickleK</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">nat_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#nat_countMixin"><span class="id" title="definition">nat_countMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="bool_countMixin"><span class="id" title="definition">bool_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#oddb"><span class="id" title="lemma">oddb</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bool_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</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 class="idref" href="mathcomp.ssreflect.choice.html#bool_countMixin"><span class="id" title="definition">bool_countMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bitseq_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">countType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#bitseq"><span class="id" title="definition">bitseq</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="unit_countMixin"><span class="id" title="definition">unit_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bool_of_unitK"><span class="id" title="lemma">bool_of_unitK</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unit_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</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.choice.html#unit_countMixin"><span class="id" title="definition">unit_countMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="option_countMixin"><span class="id" title="definition">option_countMixin</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#seq_of_optK"><span class="id" title="lemma">seq_of_optK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">option_countType</span> <span class="id" title="var">T</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#option_countMixin"><span class="id" title="definition">option_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="sig_countMixin"><span class="id" title="definition">sig_countMixin</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.choice.html#T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">of</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sig_countType</span> <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.choice.html#T"><span class="id" title="variable">T</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#sig_countMixin"><span class="id" title="definition">sig_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sig_subCountType</span> <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.choice.html#T"><span class="id" title="variable">T</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">of</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="prod_countMixin"><span class="id" title="definition">prod_countMixin</span></a> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#tag_of_pairK"><span class="id" title="lemma">tag_of_pairK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">prod_countType</span> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#prod_countMixin"><span class="id" title="definition">prod_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="sum_countMixin"><span class="id" title="definition">sum_countMixin</span></a> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#opair_of_sumK"><span class="id" title="lemma">opair_of_sumK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sum_countType</span> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#sum_countMixin"><span class="id" title="definition">sum_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tree_countMixin"><span class="id" title="definition">tree_countMixin</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#codeK"><span class="id" title="lemma">GenTree.codeK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tree_countType</span> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#tree"><span class="id" title="inductive">GenTree.tree</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#tree_countMixin"><span class="id" title="definition">tree_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableDataTypes"><span class="id" title="section">CountableDataTypes</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 |