fin n → α

Stream: general

[Reid Barton]

Is there any little library of functions around fin n → α providing a vector-style API?

[Reid Barton]

I'm wondering whether it would be worth making a def to use with dot notation, maybe finvec?

[Mario Carneiro]

I think so, in data.fin

[Reid Barton]

I found array actually exists but it seems extremely unused

[Reid Barton]

aha!

[Mario Carneiro]

array is special purpose because it is literally an array in the VM

[Adam Topaz]

Append is annoying... I've used docs#sum_fin_sum_equiv

[Reid Barton]

Yes, I was planning to use that in the implementation

[Floris van Doorn]

There is things like docs#fin.tail

[Reid Barton]

append is in fact the thing I specifically need the most

[Adam Topaz]

@Colter MacDonald and I did some ad-hoc stuff like this here

https://github.com/adamtopaz/UnivAlg/blob/master/src/ftuple.lean

[Adam Topaz]

It's not very well integrated with mathlib stuff though

[Reid Barton]

but in the generality of the dependently typed case, I would first need to be able to append the type vectors

[Reid Barton]

actually doesn't snoc already have this issue, hmm

[Reid Barton]

Oh I see, the input to snoc is the whole output type

[Reid Barton]

hmm maybe that's a good idea

[Adam Topaz]

Oh you want heterogeneous vectors!

[Reid Barton]

No, I don't

[Reid Barton]

but data.fin has them

[Adam Topaz]

Ah ok

[Reid Barton]

so I'm not sure what makes sense for mathlib now

[Reid Barton]

There's also some stuff in data.matrix.notation

[Reid Barton]

which seems to duplicate parts of data.fin except that it's homogeneous

[Reid Barton]

oh now I see vec_cons from data.matrix.notation is literally defined as fin.cons

[Adam Topaz]

@Reid Barton Did you end up doing anything with these fin n vectors that might end up in mathlib? I need to use a few such functions and don't want to duplicate work.

[Reid Barton]

Nothing that's in a usable state yet

[Adam Topaz]

Ok, thanks.