committed changes as per Issue #1589

[jamesmckinna]

New names in Data.Fin.Base , as discussed.
Knock-on consequences for Data.Fin.* Data.Vec.*, as discussed.
Passes fix-whitespace and GenerateEverything tests.
Old definitions not deleted, only deprecated.
Deprecate warning notices added.
CHANGELOG.md updated.

[JacquesCarette]

Otherwise, this is looking really good.

[MatthewDaggitt]

Thanks, looks like a great first PR! I've got a few minor niggly style comments, but apart from those looks great!

[jamesmckinna]

I have pushed the changes to my local repo; how do I now add them to the PR. or is this automagically done?

[MatthewDaggitt]

Automatically done, anything you push to the branch in your local repo gets added here 👍

[jamesmckinna]

OK, cool. But did I catch every snag? I guess I'll find out... :-)

[MatthewDaggitt]

A rogue code snippets left, but other than that looks great to me! I usually leave PRs up for approximately 7 days to give more people the chance to comment even if they're busy. After that, I'll merge it in 👍

[gallais]

We should probably pick fixities for these new definitions. The left/right associativity
is clearly set by the type but the level is more of an open design decision. It should
perhaps be tighter than _+_ and _*_ so that it interacts well with these Fin operations?

[JacquesCarette]

See README/Design/Fixity.agda for notes on how fixities in the library are currently set.

[MatthewDaggitt]

No more comments so merging in, thanks @jamesmckinna 👍