diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 22 |
2 files changed, 15 insertions, 15 deletions
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 29d1f3e..94fa2d8 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -977,7 +977,7 @@ Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := (arg_min i0 (fun i => P%B) (fun i => F)) (at level 0, i, i0 at level 10, format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : form_scope. - + Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := [arg min_(i < i0 | i \in A) F] (at level 0, i, i0 at level 10, @@ -986,12 +986,12 @@ Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] (at level 0, i, i0 at level 10, format "[ 'arg' 'min_' ( i < i0 ) F ]") : form_scope. - + Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" := (arg_max i0 (fun i => P%B) (fun i => F)) (at level 0, i, i0 at level 10, format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : form_scope. - + Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" := [arg max_(i > i0 | i \in A) F] (at level 0, i, i0 at level 10, @@ -1491,7 +1491,7 @@ Proof. exact: Finite.uniq_enumP (undup_uniq _) mem_seq_sub_enum. Qed. Definition seq_sub_finMixin := Finite.Mixin seq_sub_countMixin seq_sub_axiom. (* Beware: these are not the canonical instances, as they are not consistent *) -(* the generic sub_choiceType canonical instance. *) +(* with the generic sub_choiceType canonical instance. *) Definition adhoc_seq_sub_choiceMixin := PcanChoiceMixin seq_sub_pickleK. Definition adhoc_seq_sub_choiceType := Eval hnf in ChoiceType seq_sub adhoc_seq_sub_choiceMixin. diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 5343893..0bcfda2 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -25,7 +25,7 @@ Require Import ssrfun. (* decidable P <-> P is effectively decidable (:= {P} + {~ P}. *) (* contra, contraL, ... :: contraposition lemmas. *) (* altP my_viewP :: natural alternative for reflection; given *) -(* lemma myvieP: reflect my_Prop my_formula, *) +(* lemma myviewP: reflect my_Prop my_formula, *) (* have [myP | not_myP] := altP my_viewP. *) (* generates two subgoals, in which my_formula has *) (* been replaced by true and false, resp., with *) @@ -1329,22 +1329,22 @@ Implicit Arguments has_quality [T]. Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed. -Notation "x \is A" := (x \in has_quality 0 A) +Notation "x \is A" := (x \in has_quality 0 A) (at level 70, no associativity, format "'[hv' x '/ ' \is A ']'") : bool_scope. -Notation "x \is 'a' A" := (x \in has_quality 1 A) +Notation "x \is 'a' A" := (x \in has_quality 1 A) (at level 70, no associativity, format "'[hv' x '/ ' \is 'a' A ']'") : bool_scope. -Notation "x \is 'an' A" := (x \in has_quality 2 A) +Notation "x \is 'an' A" := (x \in has_quality 2 A) (at level 70, no associativity, format "'[hv' x '/ ' \is 'an' A ']'") : bool_scope. -Notation "x \isn't A" := (x \notin has_quality 0 A) +Notation "x \isn't A" := (x \notin has_quality 0 A) (at level 70, no associativity, format "'[hv' x '/ ' \isn't A ']'") : bool_scope. -Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) +Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) (at level 70, no associativity, format "'[hv' x '/ ' \isn't 'a' A ']'") : bool_scope. -Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) +Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) (at level 70, no associativity, format "'[hv' x '/ ' \isn't 'an' A ']'") : bool_scope. Notation "[ 'qualify' x | P ]" := (Qualifier 0 (fun x => P%B)) @@ -1411,11 +1411,11 @@ Canonical keyed_qualifier_keyed := PackKeyedPred k keyed_qualifier_suproof. End KeyedQualifier. -Notation "x \i 's' A" := (x \i n has_quality 0 A) +Notation "x \i 's' A" := (x \i n has_quality 0 A) (at level 70, format "'[hv' x '/ ' \i 's' A ']'") : bool_scope. -Notation "x \i 's' 'a' A" := (x \i n has_quality 1 A) +Notation "x \i 's' 'a' A" := (x \i n has_quality 1 A) (at level 70, format "'[hv' x '/ ' \i 's' 'a' A ']'") : bool_scope. -Notation "x \i 's' 'an' A" := (x \i n has_quality 2 A) +Notation "x \i 's' 'an' A" := (x \i n has_quality 2 A) (at level 70, format "'[hv' x '/ ' \i 's' 'an' A ']'") : bool_scope. Module DefaultKeying. @@ -1469,7 +1469,7 @@ Definition pre_symmetric := forall x y, R x y -> R y x. Lemma symmetric_from_pre : pre_symmetric -> symmetric. Proof. by move=> symR x y; apply/idP/idP; apply: symR. Qed. - + Definition reflexive := forall x, R x x. Definition irreflexive := forall x, R x x = false. |