diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index bfecfa9..bcb163c 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -162,7 +162,8 @@ Definition pi_of (n : pi_arg) : nat_pred := [pred p in primes n]. Notation "\pi ( n )" := (pi_of n) (at level 2, format "\pi ( n )") : nat_scope. -Notation "\pi ( A )" := \pi(#|A|) (only printing) : nat_scope. +Notation "\p 'i' ( A )" := \pi(#|A|) + (at level 2, format "\p 'i' ( A )") : nat_scope. Definition pdiv n := head 1 (primes n). |