refactor(data/{fin,unsigned}/*): remove unused {fin/unsigned} ops

[pechersky]

The removed fin and unsigned ops are not used in core, other than unsigned.add. Moving them to mathlib would allow them to be redefined, if need be. Test outputs were edited to remove the now-absent instances.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/fin.20ops.20and.20unsigned.20ops.20in.20core

---

As far as I can tell, these functions have no VM overrides, so it is fine to remove these from core. This is a reattempt of #525, done with checking the build locally first.

[bryangingechen]

bors try

[bors]

try

Build succeeded:

• Build macos Release
• Build linux Release
• Build macos Debug
• Build emscripten
• Build linux Debug
• Build windows Release
• Build sanitized

[bryangingechen]

LGTM. Out of curiosity, do you happen to know where unsigned.add is still used? I couldn't immediately find it by searching.

[pechersky]

It's used in init/meta/name:

/-- Reflect a C++ name object. The VM replaces it with the C++ implementation. -/
inductive name
| anonymous  : name
| mk_string  : string → name → name
| mk_numeral : unsigned → name → name

Some parts of the code supply a numeral directly for mk_numeral. I initally ripped all the unsigned/ops out, but that broke the tests/lean/run/quote1.lean at #check ``f. So I had to bring back the most basic support for numerals for unsigned.

However, I ripped out numeral support for fin, and had to change tests/lean/run/array1.lean to explicit construction of a 2 using constructor syntax.

[bryangingechen]

Right, I saw that but I wasn't sure how the add operation was used there. Maybe something in the C++?

[gebner]

Given the future of Lean 4, I don't think this is the right direction. Lean 4 has Fin in core, and it has the same operations that we will soon have in Lean 3 (see #541).