From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.ssreflect.choice.html | 299 ++++++++++++++-------------- 1 file changed, 153 insertions(+), 146 deletions(-) (limited to 'docs/htmldoc/mathcomp.ssreflect.choice.html') diff --git a/docs/htmldoc/mathcomp.ssreflect.choice.html b/docs/htmldoc/mathcomp.ssreflect.choice.html index d38d215..24fce76 100644 --- a/docs/htmldoc/mathcomp.ssreflect.choice.html +++ b/docs/htmldoc/mathcomp.ssreflect.choice.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -39,8 +38,12 @@ 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 @@ -101,31 +104,31 @@

-Definition code := foldr (fun n m ⇒ 2 ^ n × m.*2.+1) 0.
+Definition code := foldr (fun n m ⇒ 2 ^ n × m.*2.+1) 0.

-Fixpoint decode_rec (v q r : nat) {struct q} :=
+Fixpoint decode_rec (v q r : nat) {struct q} :=
  match q, r with
-  | 0, _ ⇒ [:: v]
-  | q'.+1, 0 ⇒ v :: [rec 0, q', q']
-  | q'.+1, 1 ⇒ [rec v.+1, q', q']
-  | q'.+1, r'.+2 ⇒ [rec v, q', r']
-  end where "[ 'rec' v , q , r ]" := (decode_rec v q r).
+  | 0, _ ⇒ [:: v]
+  | q'.+1, 0 ⇒ v :: [rec 0, q', q']
+  | q'.+1, 1 ⇒ [rec v.+1, q', q']
+  | q'.+1, r'.+2 ⇒ [rec v, q', r']
+  end where "[ 'rec' v , q , r ]" := (decode_rec v q r).

-Definition decode n := if n is 0 then [::] else [rec 0, n.-1, n.-1].
+Definition decode n := if n is 0 then [::] else [rec 0, n.-1, n.-1].

-Lemma decodeK : cancel decode code.
+Lemma decodeK : cancel decode code.

-Lemma codeK : cancel code decode.
+Lemma codeK : cancel code decode.

-Lemma ltn_code s : all (fun j ⇒ j < code s) s.
+Lemma ltn_code s : all (fun j ⇒ j < code s) s.

-Lemma gtn_decode n : all (ltn^~ n) (decode n).
+Lemma gtn_decode n : all (ltn^~ n) (decode n).

End CodeSeq.
@@ -149,28 +152,30 @@ Variables T T1 T2 : Type.

-Definition seq_of_opt := @oapp T _ (nseq 1) [::].
-Lemma seq_of_optK : cancel seq_of_opt ohead.
+Definition seq_of_opt := @oapp T _ (nseq 1) [::].
+Lemma seq_of_optK : cancel seq_of_opt ohead.

-Definition tag_of_pair (p : T1 × T2) := @Tagged T1 p.1 (fun _ ⇒ T2) p.2.
-Definition pair_of_tag (u : {i : T1 & T2}) := (tag u, tagged u).
-Lemma tag_of_pairK : cancel tag_of_pair pair_of_tag.
-Lemma pair_of_tagK : cancel pair_of_tag tag_of_pair.
+Definition tag_of_pair (p : T1 × T2) := @Tagged T1 p.1 (fun _ ⇒ T2) p.2.
+Definition pair_of_tag (u : {i : T1 & T2}) := (tag u, tagged u).
+Lemma tag_of_pairK : cancel tag_of_pair pair_of_tag.
+Lemma pair_of_tagK : cancel pair_of_tag tag_of_pair.

-Definition opair_of_sum (s : T1 + T2) :=
-  match s with inl x ⇒ (Some x, None) | inr y ⇒ (None, Some y) end.
+Definition opair_of_sum (s : T1 + T2) :=
+  match s with inl x ⇒ (Some x, None) | inr y ⇒ (None, Some y) end.
Definition sum_of_opair p :=
-  oapp (some \o @inr T1 T2) (omap (@inl _ T2) p.1) p.2.
-Lemma opair_of_sumK : pcancel opair_of_sum sum_of_opair.
+  oapp (some \o @inr T1 T2) (omap (@inl _ T2) p.1) p.2.
+Lemma opair_of_sumK : pcancel opair_of_sum sum_of_opair.

-Lemma bool_of_unitK : cancel (fun _ ⇒ true) (fun _ ⇒ tt).
+Lemma bool_of_unitK : cancel (fun _ ⇒ true) (fun _ ⇒ tt).

End OtherEncodings.
+
+
@@ -189,47 +194,47 @@ Variable T : Type.

-Inductive tree := Leaf of T | Node of nat & seq tree.
+Inductive tree := Leaf of T | Node of nat & seq tree.

Definition tree_rect K IH_leaf IH_node :=
  fix loop t : K t := match t with
  | Leaf x ⇒ IH_leaf x
  | Node n f0 ⇒
-    let fix iter_pair f : foldr (fun t ⇒ prod (K t)) unit f :=
-      if f is t :: f' then (loop t, iter_pair f') else tt in
+    let fix iter_pair f : foldr (fun t ⇒ prod (K t)) unit f :=
+      if f is t :: f' then (loop t, iter_pair f') else tt in
    IH_node n f0 (iter_pair f0)
  end.
-Definition tree_rec (K : tree → Set) := @tree_rect K.
+Definition tree_rec (K : tree → Set) := @tree_rect K.
Definition tree_ind K IH_leaf IH_node :=
-  fix loop t : K t : Prop := match t with
+  fix loop t : K t : Prop := match t with
  | Leaf x ⇒ IH_leaf x
  | Node n f0 ⇒
-    let fix iter_conj f : foldr (fun t ⇒ and (K t)) True f :=
-        if f is t :: f' then conj (loop t) (iter_conj f') else Logic.I
+    let fix iter_conj f : foldr (fun t ⇒ and (K t)) True f :=
+        if f is t :: f' then conj (loop t) (iter_conj f') else Logic.I
      in IH_node n f0 (iter_conj f0)
    end.

-Fixpoint encode t : seq (nat + T) :=
+Fixpoint encode t : seq (nat + T) :=
  match t with
-  | Leaf x ⇒ [:: inr _ x]
-  | Node n f ⇒ inl _ n.+1 :: rcons (flatten (map encode f)) (inl _ 0)
+  | Leaf x ⇒ [:: inr _ x]
+  | Node n f ⇒ inl _ n.+1 :: rcons (flatten (map encode f)) (inl _ 0)
  end.

Definition decode_step c fs :=
  match c with
-  | inr x ⇒ (Leaf x :: fs.1, fs.2)
-  | inl 0 ⇒ ([::], fs.1 :: fs.2)
-  | inl n.+1 ⇒ (Node n fs.1 :: head [::] fs.2, behead fs.2)
+  | inr x ⇒ (Leaf x :: fs.1, fs.2)
+  | inl 0 ⇒ ([::], fs.1 :: fs.2)
+  | inl n.+1 ⇒ (Node n fs.1 :: head [::] fs.2, behead fs.2)
  end.

-Definition decode c := ohead (foldr decode_step ([::], [::]) c).1.
+Definition decode c := ohead (foldr decode_step ([::], [::]) c).1.

-Lemma codeK : pcancel encode decode.
+Lemma codeK : pcancel encode decode.

End Def.
@@ -294,26 +299,26 @@
Record mixin_of T := Mixin {
-  find : pred T → nat → option T;
-  _ : ∀ P n x, find P n = Some x → P x;
-  _ : ∀ P : pred T, (∃ x, P x) → ∃ n, find P n;
-  _ : ∀ P Q : pred T, P =1 Q → find P =1 find Q
+  find : pred T → nat → option T;
+  _ : ∀ P n x, find P n = Some x → P x;
+  _ : ∀ P : pred T, (∃ x, P x) → ∃ n, find P n;
+  _ : ∀ P Q : pred T, P =1 Q → find P =1 find Q
}.

Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}.

-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
-Notation xclass := (class : class_of xT).
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
+Notation xclass := (class : class_of xT).

Definition pack m :=
-  fun b bT & phant_id (Equality.class bT) b ⇒ Pack (@Class T b m) T.
+  fun b bT & phant_id (Equality.class bT) b ⇒ Pack (@Class T b m).

@@ -322,7 +327,7 @@ Inheritance
-Definition eqType := @Equality.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.

End ClassDef.
@@ -335,10 +340,10 @@ Canonical eqType.
Notation choiceType := type.
Notation choiceMixin := mixin_of.
-Notation ChoiceType T m := (@pack T m _ _ id).
-Notation "[ 'choiceType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
+Notation ChoiceType T m := (@pack T m _ _ id).
+Notation "[ 'choiceType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'choiceType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'choiceType' 'of' T ]" := (@clone T _ _ id)
+Notation "[ 'choiceType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'choiceType' 'of' T ]") : form_scope.

@@ -357,19 +362,19 @@
Variable T : choiceType.
-Implicit Types P Q : pred T.
+Implicit Types P Q : pred T.

-Lemma correct P n x : find P n = Some x → P x.
+Lemma correct P n x : find P n = Some x → P x.

-Lemma complete P : (∃ x, P x) → (∃ n, find P n).
+Lemma complete P : (∃ x, P x) → (∃ n, find P n).

-Lemma extensional P Q : P =1 Q → find P =1 find Q.
+Lemma extensional P Q : P =1 Q → find P =1 find Q.

-Fact xchoose_subproof P exP : {x | find P (ex_minn (@complete P exP)) = Some x}.
+Fact xchoose_subproof P exP : {x | find P (ex_minn (@complete P exP)) = Some x}.

End InternalTheory.
@@ -391,7 +396,7 @@
Variable T : choiceType.
-Implicit Types P Q : pred T.
+Implicit Types P Q : pred T.

Definition xchoose P exP := sval (@xchoose_subproof T P exP).
@@ -400,49 +405,49 @@ Lemma xchooseP P exP : P (@xchoose P exP).

-Lemma eq_xchoose P Q exP exQ : P =1 Q → @xchoose P exP = @xchoose Q exQ.
+Lemma eq_xchoose P Q exP exQ : P =1 Q → @xchoose P exP = @xchoose Q exQ.

-Lemma sigW P : (∃ x, P x) → {x | P x}.
+Lemma sigW P : (∃ x, P x) → {x | P x}.

-Lemma sig2W P Q : (exists2 x, P x & Q x) → {x | P x & Q x}.
+Lemma sig2W P Q : (exists2 x, P x & Q x) → {x | P x & Q x}.

-Lemma sig_eqW (vT : eqType) (lhs rhs : T → vT) :
-  (∃ x, lhs x = rhs x) → {x | lhs x = rhs x}.
+Lemma sig_eqW (vT : eqType) (lhs rhs : T → vT) :
+  (∃ x, lhs x = rhs x) → {x | lhs x = rhs x}.

-Lemma sig2_eqW (vT : eqType) (P : pred T) (lhs rhs : T → vT) :
-  (exists2 x, P x & lhs x = rhs x) → {x | P x & lhs x = rhs x}.
+Lemma sig2_eqW (vT : eqType) (P : pred T) (lhs rhs : T → vT) :
+  (exists2 x, P x & lhs x = rhs x) → {x | P x & lhs x = rhs x}.

Definition choose P x0 :=
-  if insub x0 : {? x | P x} is Some (exist x Px) then
-    xchoose (ex_intro [eta P] x Px)
+  if insub x0 : {? x | P x} is Some (exist x Px) then
+    xchoose (ex_intro [eta P] x Px)
  else x0.

-Lemma chooseP P x0 : P x0 → P (choose P x0).
+Lemma chooseP P x0 : P x0 → P (choose P x0).

-Lemma choose_id P x0 y0 : P x0 → P y0 → choose P x0 = choose P y0.
+Lemma choose_id P x0 y0 : P x0 → P y0 → choose P x0 = choose P y0.

-Lemma eq_choose P Q : P =1 Q → choose P =1 choose Q.
+Lemma eq_choose P Q : P =1 Q → choose P =1 choose Q.

Section CanChoice.

-Variables (sT : Type) (f : sT → T).
+Variables (sT : Type) (f : sT → T).

-Lemma PcanChoiceMixin f' : pcancel f f' → choiceMixin sT.
+Lemma PcanChoiceMixin f' : pcancel f f' → choiceMixin sT.

-Definition CanChoiceMixin f' (fK : cancel f f') :=
-  PcanChoiceMixin (can_pcan fK).
+Definition CanChoiceMixin f' (fK : cancel f f') :=
+  PcanChoiceMixin (can_pcan fK).

End CanChoice.
@@ -451,12 +456,12 @@ Section SubChoice.

-Variables (P : pred T) (sT : subType P).
+Variables (P : pred T) (sT : subType P).

Definition sub_choiceMixin := PcanChoiceMixin (@valK T P sT).
Definition sub_choiceClass := @Choice.Class sT (sub_eqMixin sT) sub_choiceMixin.
-Canonical sub_choiceType := Choice.Pack sub_choiceClass sT.
+Canonical sub_choiceType := Choice.Pack sub_choiceClass.

End SubChoice.
@@ -472,49 +477,49 @@ Section TagChoice.

-Variables (I : choiceType) (T_ : I → choiceType).
+Variables (I : choiceType) (T_ : I → choiceType).

-Fact tagged_choiceMixin : choiceMixin {i : I & T_ i}.
+Fact tagged_choiceMixin : choiceMixin {i : I & T_ i}.
Canonical tagged_choiceType :=
-  Eval hnf in ChoiceType {i : I & T_ i} tagged_choiceMixin.
+  Eval hnf in ChoiceType {i : I & T_ i} tagged_choiceMixin.

End TagChoice.

-Fact nat_choiceMixin : choiceMixin nat.
-Canonical nat_choiceType := Eval hnf in ChoiceType nat nat_choiceMixin.
+Fact nat_choiceMixin : choiceMixin nat.
+Canonical nat_choiceType := Eval hnf in ChoiceType nat nat_choiceMixin.

Definition bool_choiceMixin := CanChoiceMixin oddb.
-Canonical bool_choiceType := Eval hnf in ChoiceType bool bool_choiceMixin.
-Canonical bitseq_choiceType := Eval hnf in [choiceType of bitseq].
+Canonical bool_choiceType := Eval hnf in ChoiceType bool bool_choiceMixin.
+Canonical bitseq_choiceType := Eval hnf in [choiceType of bitseq].

Definition unit_choiceMixin := CanChoiceMixin bool_of_unitK.
-Canonical unit_choiceType := Eval hnf in ChoiceType unit unit_choiceMixin.
+Canonical unit_choiceType := Eval hnf in ChoiceType unit unit_choiceMixin.

Definition option_choiceMixin T := CanChoiceMixin (@seq_of_optK T).
Canonical option_choiceType T :=
-  Eval hnf in ChoiceType (option T) (option_choiceMixin T).
+  Eval hnf in ChoiceType (option T) (option_choiceMixin T).

-Definition sig_choiceMixin T (P : pred T) : choiceMixin {x | P x} :=
+Definition sig_choiceMixin T (P : pred T) : choiceMixin {x | P x} :=
   sub_choiceMixin _.
-Canonical sig_choiceType T (P : pred T) :=
- Eval hnf in ChoiceType {x | P x} (sig_choiceMixin P).
+Canonical sig_choiceType T (P : pred T) :=
+ Eval hnf in ChoiceType {x | P x} (sig_choiceMixin P).

Definition prod_choiceMixin T1 T2 := CanChoiceMixin (@tag_of_pairK T1 T2).
Canonical prod_choiceType T1 T2 :=
-  Eval hnf in ChoiceType (T1 × T2) (prod_choiceMixin T1 T2).
+  Eval hnf in ChoiceType (T1 × T2) (prod_choiceMixin T1 T2).

Definition sum_choiceMixin T1 T2 := PcanChoiceMixin (@opair_of_sumK T1 T2).
Canonical sum_choiceType T1 T2 :=
-  Eval hnf in ChoiceType (T1 + T2) (sum_choiceMixin T1 T2).
+  Eval hnf in ChoiceType (T1 + T2) (sum_choiceMixin T1 T2).

Definition tree_choiceMixin T := PcanChoiceMixin (GenTree.codeK T).
@@ -524,8 +529,8 @@ End ChoiceTheory.

-Notation "[ 'choiceMixin' 'of' T 'by' <: ]" :=
-  (sub_choiceMixin _ : choiceMixin T)
+Notation "[ 'choiceMixin' 'of' T 'by' <: ]" :=
+  (sub_choiceMixin _ : choiceMixin T)
  (at level 0, format "[ 'choiceMixin' 'of' T 'by' <: ]") : form_scope.

@@ -533,9 +538,9 @@
Record mixin_of (T : Type) : Type := Mixin {
-  pickle : T → nat;
-  unpickle : nat → option T;
-  pickleK : pcancel pickle unpickle
+  pickle : T → nat;
+  unpickle : nat → option T;
+  pickleK : pcancel pickle unpickle
}.

@@ -549,20 +554,20 @@ Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }.

-Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
+Structure type : Type := Pack {sort : Type; _ : class_of sort}.
Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
-Notation xclass := (class : class_of xT).
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
+Notation xclass := (class : class_of xT).

Definition pack m :=
-  fun bT b & phant_id (Choice.class bT) b ⇒ Pack (@Class T b m) T.
+  fun bT b & phant_id (Choice.class bT) b ⇒ Pack (@Class T b m).

-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.

End ClassDef.
@@ -577,12 +582,12 @@ Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Notation countType := type.
-Notation CountType T m := (@pack T m _ _ id).
+Notation CountType T m := (@pack T m _ _ id).
Notation CountMixin := Mixin.
Notation CountChoiceMixin := ChoiceMixin.
-Notation "[ 'countType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
+Notation "[ 'countType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
 (at level 0, format "[ 'countType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'countType' 'of' T ]" := (@clone T _ _ id)
+Notation "[ 'countType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'countType' 'of' T ]") : form_scope.

@@ -603,37 +608,37 @@ Variable T : countType.

-Lemma pickleK : @pcancel nat T pickle unpickle.
+Lemma pickleK : @pcancel nat T pickle unpickle.

Definition pickle_inv n :=
-  obind (fun x : T ⇒ if pickle x == n then Some x else None) (unpickle n).
+  obind (fun x : T ⇒ if pickle x == n then Some x else None) (unpickle n).

-Lemma pickle_invK : ocancel pickle_inv pickle.
+Lemma pickle_invK : ocancel pickle_inv pickle.

-Lemma pickleK_inv : pcancel pickle pickle_inv.
+Lemma pickleK_inv : pcancel pickle pickle_inv.

Lemma pcan_pickleK sT f f' :
-  @pcancel T sT f f' → pcancel (pickle \o f) (pcomp f' unpickle).
+  @pcancel T sT f f' → pcancel (pickle \o f) (pcomp f' unpickle).

-Definition PcanCountMixin sT f f' (fK : pcancel f f') :=
+Definition PcanCountMixin sT f f' (fK : pcancel f f') :=
  @CountMixin sT _ _ (pcan_pickleK fK).

-Definition CanCountMixin sT f f' (fK : cancel f f') :=
-  @PcanCountMixin sT _ _ (can_pcan fK).
+Definition CanCountMixin sT f f' (fK : cancel f f') :=
+  @PcanCountMixin sT _ _ (can_pcan fK).

Definition sub_countMixin P sT := PcanCountMixin (@valK T P sT).

Definition pickle_seq s := CodeSeq.code (map (@pickle T) s).
-Definition unpickle_seq n := Some (pmap (@unpickle T) (CodeSeq.decode n)).
-Lemma pickle_seqK : pcancel pickle_seq unpickle_seq.
+Definition unpickle_seq n := Some (pmap (@unpickle T) (CodeSeq.decode n)).
+Lemma pickle_seqK : pcancel pickle_seq unpickle_seq.

Definition seq_countMixin := CountMixin pickle_seqK.
@@ -643,15 +648,17 @@ End CountableTheory.

-Notation "[ 'countMixin' 'of' T 'by' <: ]" :=
-    (sub_countMixin _ : Countable.mixin_of T)
+Notation "[ 'countMixin' 'of' T 'by' <: ]" :=
+    (sub_countMixin _ : Countable.mixin_of T)
  (at level 0, format "[ 'countMixin' 'of' T 'by' <: ]") : form_scope.
+
+
Section SubCountType.

-Variables (T : choiceType) (P : pred T).
+Variables (T : choiceType) (P : pred T).
Import Countable.

@@ -660,13 +667,13 @@
Coercion sub_countType (sT : subCountType) :=
-  Eval hnf in pack (let: SubCountType _ m := sT return mixin_of sT in m) id.
+  Eval hnf in pack (let: SubCountType _ m := sT return mixin_of sT in m) id.
Canonical sub_countType.

Definition pack_subCountType U :=
-  fun sT cT & sub_sort sT × sort cT → U × U ⇒
-  fun b m & phant_id (Class b m) (class cT) ⇒ @SubCountType sT m.
+  fun sT cT & sub_sort sT × sort cT → U × U ⇒
+  fun b m & phant_id (Class b m) (class cT) ⇒ @SubCountType sT m.

End SubCountType.
@@ -678,28 +685,28 @@ This assumes that T has both countType and subType structures.
-Notation "[ 'subCountType' 'of' T ]" :=
-    (@pack_subCountType _ _ T _ _ id _ _ id)
+Notation "[ 'subCountType' 'of' T ]" :=
+    (@pack_subCountType _ _ T _ _ id _ _ id)
  (at level 0, format "[ 'subCountType' 'of' T ]") : form_scope.

Section TagCountType.

-Variables (I : countType) (T_ : I → countType).
+Variables (I : countType) (T_ : I → countType).

-Definition pickle_tagged (u : {i : I & T_ i}) :=
-  CodeSeq.code [:: pickle (tag u); pickle (tagged u)].
+Definition pickle_tagged (u : {i : I & T_ i}) :=
+  CodeSeq.code [:: pickle (tag u); pickle (tagged u)].
Definition unpickle_tagged s :=
-  if CodeSeq.decode s is [:: ni; nx] then
-    obind (fun i ⇒ omap (@Tagged I i T_) (unpickle nx)) (unpickle ni)
-  else None.
-Lemma pickle_taggedK : pcancel pickle_tagged unpickle_tagged.
+  if CodeSeq.decode s is [:: ni; nx] then
+    obind (fun i ⇒ omap (@Tagged I i T_) (unpickle nx)) (unpickle ni)
+  else None.
+Lemma pickle_taggedK : pcancel pickle_tagged unpickle_tagged.

Definition tag_countMixin := CountMixin pickle_taggedK.
-Canonical tag_countType := Eval hnf in CountType {i : I & T_ i} tag_countMixin.
+Canonical tag_countType := Eval hnf in CountType {i : I & T_ i} tag_countMixin.

End TagCountType.
@@ -717,40 +724,40 @@ Implicit Type T : countType.

-Lemma nat_pickleK : pcancel id (@Some nat).
+Lemma nat_pickleK : pcancel id (@Some nat).
Definition nat_countMixin := CountMixin nat_pickleK.
-Canonical nat_countType := Eval hnf in CountType nat nat_countMixin.
+Canonical nat_countType := Eval hnf in CountType nat nat_countMixin.

Definition bool_countMixin := CanCountMixin oddb.
-Canonical bool_countType := Eval hnf in CountType bool bool_countMixin.
-Canonical bitseq_countType := Eval hnf in [countType of bitseq].
+Canonical bool_countType := Eval hnf in CountType bool bool_countMixin.
+Canonical bitseq_countType := Eval hnf in [countType of bitseq].

Definition unit_countMixin := CanCountMixin bool_of_unitK.
-Canonical unit_countType := Eval hnf in CountType unit unit_countMixin.
+Canonical unit_countType := Eval hnf in CountType unit unit_countMixin.

Definition option_countMixin T := CanCountMixin (@seq_of_optK T).
Canonical option_countType T :=
-  Eval hnf in CountType (option T) (option_countMixin T).
+  Eval hnf in CountType (option T) (option_countMixin T).

-Definition sig_countMixin T (P : pred T) := [countMixin of {x | P x} by <:].
-Canonical sig_countType T (P : pred T) :=
-  Eval hnf in CountType {x | P x} (sig_countMixin P).
-Canonical sig_subCountType T (P : pred T) :=
-  Eval hnf in [subCountType of {x | P x}].
+Definition sig_countMixin T (P : pred T) := [countMixin of {x | P x} by <:].
+Canonical sig_countType T (P : pred T) :=
+  Eval hnf in CountType {x | P x} (sig_countMixin P).
+Canonical sig_subCountType T (P : pred T) :=
+  Eval hnf in [subCountType of {x | P x}].

Definition prod_countMixin T1 T2 := CanCountMixin (@tag_of_pairK T1 T2).
Canonical prod_countType T1 T2 :=
-  Eval hnf in CountType (T1 × T2) (prod_countMixin T1 T2).
+  Eval hnf in CountType (T1 × T2) (prod_countMixin T1 T2).

Definition sum_countMixin T1 T2 := PcanCountMixin (@opair_of_sumK T1 T2).
Canonical sum_countType T1 T2 :=
-  Eval hnf in CountType (T1 + T2) (sum_countMixin T1 T2).
+  Eval hnf in CountType (T1 + T2) (sum_countMixin T1 T2).

Definition tree_countMixin T := PcanCountMixin (GenTree.codeK T).
-- cgit v1.2.3