Add fin notations

CHANGELOG.md

@@ -67,6 +67,8 @@ longer supported by this release.
   (`map_fold` used to be derived from `map_to_list`.) This makes it possible to
   use `map_fold` in nested-recursive definitions on maps. For example,
   `Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts`.
+- Make `fin` number literal notations work with numbers above 10. (by Thibaut
+  Pérami)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

stdpp/fin.v

@@ -19,12 +19,10 @@ Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
 Global Arguments Fin.FS _ _%fin : assert.
 
-Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
-Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.
-Notation "4" := (FS 3) : fin_scope. Notation "5" := (FS 4) : fin_scope.
-Notation "6" := (FS 5) : fin_scope. Notation "7" := (FS 6) : fin_scope.
-Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope.
-Notation "10" := (FS 9) : fin_scope.
+(** Allow any non-negative number literal to be parsed as a [fin]. For example
+[42%fin : fin 64], or [42%fin : fin _], or [42%fin : fin (43 + _)]. *)
+Number Notation fin Nat.of_num_uint Nat.to_num_uint (via nat
+  mapping [[Fin.F1] => O, [Fin.FS] => S]) : fin_scope.
 
 Fixpoint fin_to_nat {n} (i : fin n) : nat :=
   match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.