From 7c47bab45686e90ee50e6c7eaae3230cb7ce9e53 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 20 Nov 2020 03:10:59 +0100 Subject: Using Arguments / to deal with volatile definitions --- mathcomp/character/character.v | 6 +++--- mathcomp/character/classfun.v | 9 ++++----- 2 files changed, 7 insertions(+), 8 deletions(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index e7ea1e0..c45dc07 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -508,8 +508,8 @@ Lemma xcfunZr a phi A : xcfun phi (a *: A) = a * xcfun phi A. Proof. by rewrite /xcfun linearZ -scalemxAl mxE. Qed. (* In order to add a second canonical structure on xcfun *) -Definition xcfun_r_head k A phi := let: tt := k in xcfun phi A. -Local Notation xcfun_r A := (xcfun_r_head tt A). +Definition xcfun_r A phi := xcfun phi A. +Arguments xcfun_r A phi /. Lemma xcfun_rE A chi : xcfun_r A chi = xcfun chi A. Proof. by []. Qed. @@ -534,7 +534,7 @@ by congr (_ * \tr _) => {A} /=; rewrite /gring_mx /= -rowE rowK mxvecK. Qed. End Char. -Notation xcfun_r A := (xcfun_r_head tt A). +Arguments xcfun_r {_ _} A phi /. Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope. Definition pred_Nirr gT B := #|@classes gT B|.-1. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index ccfc37b..d9d3476 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -378,8 +378,8 @@ Definition cfun_base A : #|classes B ::&: A|.-tuple classfun := Definition classfun_on A := <>%VS. Definition cfdot phi psi := #|B|%:R^-1 * \sum_(x in B) phi x * (psi x)^*. -Definition cfdotr_head k psi phi := let: tt := k in cfdot phi psi. -Definition cfnorm_head k phi := let: tt := k in cfdot phi phi. +Definition cfdotr psi phi := cfdot phi psi. +Definition cfnorm phi := cfdot phi phi. Coercion seq_of_cfun phi := [:: phi]. @@ -395,7 +395,8 @@ Arguments cfun_indicator {gT} B%g. Arguments cfAut {gT B%g} u phi%CF. Arguments cfReal {gT B%g} phi%CF. Arguments cfdot {gT B%g} phi%CF psi%CF. -Arguments cfdotr_head {gT B%g} k psi%CF phi%CF. +Arguments cfdotr {gT B%g} psi%CF phi%CF /. +Arguments cfnorm {gT B%g} phi%CF /. Notation "''CF' ( G )" := (classfun G) : type_scope. Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope. @@ -414,8 +415,6 @@ Notation "''[' u , v ]_ G":= (@cfdot _ G u v) (only parsing) : ring_scope. Notation "''[' u , v ]" := (cfdot u v) : ring_scope. Notation "''[' u ]_ G" := '[u, u]_G (only parsing) : ring_scope. Notation "''[' u ]" := '[u, u] : ring_scope. -Notation cfdotr := (cfdotr_head tt). -Notation cfnorm := (cfnorm_head tt). Section Predicates. -- cgit v1.2.3