diff options
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index fb4ba3d..b1498cd 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -11,8 +11,16 @@ From Coq Require Export ssrbool. (* This file also anticipates a v8.11 change in the definition of simpl_pred *) (* to T -> simpl_pred T. This change ensures that inE expands the definition *) (* of r : simpl_rel along with the \in, when rewriting in y \in r x. *) +(* *) +(* This file also anticipates v8.13 additions as well as a generalization in *) +(* the statments of `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, *) +(* monoRL_in, and can_mono_in. *) (******************************************************************************) +(******************) +(* v8.11 addtions *) +(******************) + Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0, format "{ 'pred' T }") : type_scope. @@ -50,6 +58,10 @@ Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)). Definition relpre {T rT} (f : T -> rT) (r : rel rT) := [rel x y | r (f x) (f y)]. +(******************) +(* v8.13 addtions *) +(******************) + Section HomoMonoMorphismFlip. Variables (aT rT : Type) (aR : rel aT) (rR : rel rT) (f : aT -> rT). Variable (aD aD' : {pred aT}). @@ -190,4 +202,3 @@ End inj_can_sym_in_on. Arguments inj_can_sym_in_on {aT rT aD rD f g}. Arguments inj_can_sym_on {aT rT aD f g}. Arguments inj_can_sym_in {aT rT rD f g}. - |