[Merged by Bors] - feat: port Data.Fin.VecNotation

[jcommelin]

---

• feat: port Data.Fin.VecNotation
• Initial file copy from mathport
• automated fixes

[urkud]

I'm going to fix lint errors. UPD: done. Should we backport the only API change? Do we need the whole section about bit0/bit1 or should we just #noalign all these lemmas?

[jcommelin]

bors d=Ruben-VandeVelde

[Ruben-VandeVelde]

Should we backport the only API change?

Done in leanprover-community/mathlib#18259

Do we need the whole section about bit0/bit1 or should we just #noalign all these lemmas?

Keep them for now

[eric-wieser]

Should we backport the only API change?

Why was an API change made in the port? The change itself looks fine, but I don't think we should do this type of thing without at least explaining why in the PR description.

[eric-wieser]

Note that it would be a dsimp lemma if we had

def Nat.ble : @& Nat → @& Nat → Bool
  | zero,   _      => true
  | succ _, zero   => false
  | succ n, succ m => ble n m

instead of

def Nat.ble : @& Nat → @& Nat → Bool
  | zero,   zero   => true
  | zero,   succ _ => true
  | succ _, zero   => false
  | succ n, succ m => ble n m

[urkud]

Should we backport the only API change?

Why was an API change made in the port? The change itself looks fine, but I don't think we should do this type of thing without at least explaining why in the PR description.

There was a linter error about an unused have. While fixing it, I made this change for no reason better than "we should make this change some day, why not today?".

[jcommelin]

This file is currently blocking progress.

[jcommelin]

@urkud are you ok with reverting the API change and leaving a TODO?

[Ruben-VandeVelde]

bors r+

[bors]

🔒 Permission denied

Existing reviewers: click here to make Ruben-VandeVelde a reviewer

[urkud]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style