(* * Notations for Fin.t *)
(* Author: Maximilian Wuttke *)

From Undecidability.Shared.Libs.PSL Require Import Fin.

Notation "'Fin0'" := (Fin.F1).
Notation "'Fin1'" := (Fin.FS ).
Notation "'Fin2'" := (Fin.FS ).
Notation "'Fin3'" := (Fin.FS ).
Notation "'Fin4'" := (Fin.FS ).
Notation "'Fin5'" := (Fin.FS ).
Notation "'Fin6'" := (Fin.FS ).
Notation "'Fin7'" := (Fin.FS ).
Notation "'Fin8'" := (Fin.FS ).
Notation "'Fin9'" := (Fin.FS ).
Notation "'Fin10'" := (Fin.FS ).
Notation "'Fin11'" := (Fin.FS ).
Notation "'Fin12'" := (Fin.FS ).
Notation "'Fin13'" := (Fin.FS ).
Notation "'Fin14'" := (Fin.FS ).
Notation "'Fin15'" := (Fin.FS ).
Notation "'Fin16'" := (Fin.FS ).
Notation "'Fin17'" := (Fin.FS ).
Notation "'Fin18'" := (Fin.FS ).
Notation "'Fin19'" := (Fin.FS ).
Notation "'Fin20'" := (Fin.FS ).
Notation "'Fin21'" := (Fin.FS ).
Notation "'Fin22'" := (Fin.FS ).
Notation "'Fin23'" := (Fin.FS ).
Notation "'Fin24'" := (Fin.FS ).
Notation "'Fin25'" := (Fin.FS ).
Notation "'Fin26'" := (Fin.FS ).
Notation "'Fin27'" := (Fin.FS ).
Notation "'Fin28'" := (Fin.FS ).
Notation "'Fin29'" := (Fin.FS ).
Notation "'Fin30'" := (Fin.FS ).
Notation "'Fin31'" := (Fin.FS ).
Notation "'Fin32'" := (Fin.FS ).
Notation "'Fin33'" := (Fin.FS ).
Notation "'Fin34'" := (Fin.FS ).
Notation "'Fin35'" := (Fin.FS ).
Notation "'Fin36'" := (Fin.FS ).
Notation "'Fin37'" := (Fin.FS ).
Notation "'Fin38'" := (Fin.FS ).
Notation "'Fin39'" := (Fin.FS ).
Notation "'Fin40'" := (Fin.FS ).
Notation "'Fin41'" := (Fin.FS ).
Notation "'Fin42'" := (Fin.FS ).
Notation "'Fin43'" := (Fin.FS ).
Notation "'Fin44'" := (Fin.FS ).
Notation "'Fin45'" := (Fin.FS ).
Notation "'Fin46'" := (Fin.FS ).
Notation "'Fin47'" := (Fin.FS ).
Notation "'Fin48'" := (Fin.FS ).
Notation "'Fin49'" := (Fin.FS ).
Notation "'Fin50'" := (Fin.FS ).
Notation "'Fin51'" := (Fin.FS ).
Notation "'Fin52'" := (Fin.FS ).
Notation "'Fin53'" := (Fin.FS ).
Notation "'Fin54'" := (Fin.FS ).
Notation "'Fin55'" := (Fin.FS ).
Notation "'Fin56'" := (Fin.FS ).
Notation "'Fin57'" := (Fin.FS ).
Notation "'Fin58'" := (Fin.FS ).
Notation "'Fin59'" := (Fin.FS ).
Notation "'Fin60'" := (Fin.FS ).
Notation "'Fin61'" := (Fin.FS ).
Notation "'Fin62'" := (Fin.FS ).
Notation "'Fin63'" := (Fin.FS ).
Notation "'Fin64'" := (Fin.FS ).
Notation "'Fin65'" := (Fin.FS ).
Notation "'Fin66'" := (Fin.FS ).
Notation "'Fin67'" := (Fin.FS ).
Notation "'Fin68'" := (Fin.FS ).
Notation "'Fin69'" := (Fin.FS ).
Notation "'Fin70'" := (Fin.FS ).
Notation "'Fin71'" := (Fin.FS ).
Notation "'Fin72'" := (Fin.FS ).
Notation "'Fin73'" := (Fin.FS ).
Notation "'Fin74'" := (Fin.FS ).
Notation "'Fin75'" := (Fin.FS ).
Notation "'Fin76'" := (Fin.FS ).
Notation "'Fin77'" := (Fin.FS ).
Notation "'Fin78'" := (Fin.FS ).
Notation "'Fin79'" := (Fin.FS ).
Notation "'Fin80'" := (Fin.FS ).
Notation "'Fin81'" := (Fin.FS ).
Notation "'Fin82'" := (Fin.FS ).
Notation "'Fin83'" := (Fin.FS ).
Notation "'Fin84'" := (Fin.FS ).
Notation "'Fin85'" := (Fin.FS ).
Notation "'Fin86'" := (Fin.FS ).
Notation "'Fin87'" := (Fin.FS ).
Notation "'Fin88'" := (Fin.FS ).
Notation "'Fin89'" := (Fin.FS ).
Notation "'Fin90'" := (Fin.FS ).
Notation "'Fin91'" := (Fin.FS ).
Notation "'Fin92'" := (Fin.FS ).
Notation "'Fin93'" := (Fin.FS ).
Notation "'Fin94'" := (Fin.FS ).
Notation "'Fin95'" := (Fin.FS ).
Notation "'Fin96'" := (Fin.FS ).
Notation "'Fin97'" := (Fin.FS ).
Notation "'Fin98'" := (Fin.FS ).
Notation "'Fin99'" := (Fin.FS ).

(* Generate arbitrary big Fin.t's *)

Ltac getFin i :=
  match i with
  | 0
    eapply Fin.F1
  | S ?i'
    eapply Fin.FS;
    ltac:(getFin i')
  end.

(*
Section Test.
  Compute ltac:(getFin 4) : Fin.t 100.
  Compute ltac:(getFin 8) : Fin.t 100.
  Compute ltac:(getFin 15) : Fin.t 100.
  Compute ltac:(getFin 16) : Fin.t 100.
  Compute ltac:(getFin 23) : Fin.t 100.
  Compute ltac:(getFin 42) : Fin.t 100.
End Test.
*)