diff options
| author | Kazuhiko Sakaguchi | 2018-07-12 20:19:55 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2018-07-12 20:19:55 +0900 |
| commit | 10171942883948c8144ec076ef48eb73f8e49cdd (patch) | |
| tree | e5e5f5ff58fd3b3c07afd49388afcab5cbbe165b /mathcomp/ssreflect/eqtype.v | |
| parent | b8be28130d6a2a057858e3978c75ee0796630dce (diff) | |
Replace all the CoInductives with Variants
Diffstat (limited to 'mathcomp/ssreflect/eqtype.v')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 159c00e..01ce7a9 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -420,7 +420,7 @@ Section FunWith. Variables (aT : eqType) (rT : Type). -CoInductive fun_delta : Type := FunDelta of aT & rT. +Variant fun_delta : Type := FunDelta of aT & rT. Definition fwith x y (f : aT -> rT) := [fun z => if z == x then y else f z]. @@ -501,7 +501,7 @@ Definition clone_subType U v := Variable sT : subType. -CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). +Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). Lemma SubP u : Sub_spec u. Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed. @@ -514,7 +514,7 @@ Definition insub x := Definition insubd u0 x := odflt u0 (insub x). -CoInductive insub_spec x : option sT -> Type := +Variant insub_spec x : option sT -> Type := | InsubSome u of P x & val u = x : insub_spec x (Some u) | InsubNone of ~~ P x : insub_spec x None. |