diff options
| author | Georges Gonthier | 2019-04-28 20:37:17 +0200 |
|---|---|---|
| committer | Georges Gonthier | 2019-04-29 00:26:36 +0200 |
| commit | 6be8fd5c67949a59bde7083e81401263986e7a4e (patch) | |
| tree | 71a6e45e4948db3a459906982a5b2b982470108c /mathcomp/algebra/vector.v | |
| parent | 8e27a1dd704c8f7a34de29d65337eb67254a1741 (diff) | |
Generalise use of `{pred T}` from coq/coq#9995
Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).
Diffstat (limited to 'mathcomp/algebra/vector.v')
| -rw-r--r-- | mathcomp/algebra/vector.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 48d7d3e..e73ca33 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -267,10 +267,10 @@ Definition subsetv U V := (vs2mx U <= vs2mx V)%MS. Definition vline u := mx2vs (v2r u). (* Vspace membership is defined as line inclusion. *) -Definition pred_of_vspace phV (U : Vector.space phV) : pred_class := +Definition pred_of_vspace phV (U : Vector.space phV) : {pred vT} := fun v => (vs2mx (vline v) <= vs2mx U)%MS. Canonical vspace_predType := - @mkPredType _ (unkeyed {vspace vT}) (@pred_of_vspace _). + @PredType _ (unkeyed {vspace vT}) (@pred_of_vspace _). Definition fullv : {vspace vT} := mx2vs 1%:M. Definition addv U V := mx2vs (vs2mx U + vs2mx V). @@ -294,7 +294,7 @@ Definition basis_of U X := (span X == U) && free X. End VspaceDefs. -Coercion pred_of_vspace : Vector.space >-> pred_class. +Coercion pred_of_vspace : Vector.space >-> pred_sort. Notation "\dim U" := (dimv U) : nat_scope. Notation "U <= V" := (subsetv U V) : vspace_scope. Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope. |