SafeIdx: a beginner-friendly library

Stream: new members

[Adrien Champion]

I just published my SafeIdx library :smile:

• https://github.com/AdrienChampion/safeIdx

It basically generates Uid types that are just wrappers around Nat, and Uid-related mappings which are just arrays only indexable by a specific Uid type. The result is (hopefully) zero-cost arrays and indices, except that type-safety prevents from using, say, a Client index instead of a Product index in a Product-related mapping.
Because this is Lean, SafeIdx also provides dependent (length-aware) mapping types which is super fun to write.

Check out what it looks like on this example:

• https://github.com/AdrienChampion/safeIdx/blob/9e585005f83162b067be2a7702376b520bfc7c44/SafeIdx/Test/Client.lean

[Adrien Champion]

I'm not here to argue that's the most useful library ever :smile: But it might be interesting to others; I find the exercise of writing/reading such a library very valuable for beginners as it's not very ambitious so it's easy to grasp the concepts, but still requires playing around with types, relatively low-level array manipulations, coercion, custom-indexing, syntax extensions, and much more. It should also ideally be zero-cost, so there's even room for messing around with optimization.

There's even a (very simple) termination proof in there!

[Adrien Champion]

Also, I'm definitely not a Lean expert so any remarks for improving readability/ergonomics or anything else would be great.

Feel free to start with this hideous bit and let me know how to do this cleanly once you're done laughing