From 5d7bd2ea2a0a28fb275da8ba2e2c0dc5a33d1034 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Wed, 8 May 2019 09:43:34 +0200 Subject: refactor `seq` permutation theory - Change the naming of permutation lemmas so they conform to a consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`) prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq` using a property when there is also a lemma _using_ `perm_eq` for the same property. Lemmas that do not concern `perm_eq` do _not_ have `perm` in their name. - Change the definition of `permutations` for a time- and space- back-to-front generation algorithm. - Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and `tally_seq`, used by the improved `permutation` algorithm. - add deprecated aliases for renamed lemmas --- mathcomp/ssreflect/ssreflect.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'mathcomp/ssreflect/ssreflect.v') diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 95da9cd..2925496 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -17,6 +17,15 @@ Global Set Bullet Behavior "None". (* --> Usage: Notation old := (deprecate old new) (only parsing). *) (* --> Caveat: deprecate old new only inherits new's maximal implicits; *) (* on-demand implicits should be added after : (deprecate old new _). *) +(* --> Caveat 2: if premises or conclusions need to be adjusted, of for *) +(* non-prenex implicits, use the idiom: *) +(* Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...) *) +(* _ _ ... _) (only printing). *) +(* where all the implicit a_i's occur first, and correspond to the *) +(* trailing _'s, making sure deprecate old new is fully applied and *) +(* there are _no implicits_ inside the (fun .. => ..) expression. This *) +(* is to avoid triggering a bug in SSReflect elaboration that is *) +(* triggered by such evars under binders. *) (* Import Deprecation.Silent :: turn off deprecation warning messages. *) (* Import Deprecation.Reject :: raise an error instead of only warning. *) (******************************************************************************) -- cgit v1.2.3