How to use Fin.cons

Stream: new members

[Vivek Rajesh Joshi]

I want to append a function on Fin with an element from the left. I searched for such a function and found Fin.cons, but I don't understand how to get it to work. Can anyone tell me what my inputs to the function must be?
(I have copy-pasted it as fin_cons here)

import Mathlib.Data.Matrix.Notation

variable {α : Fin (n + 1) → Type u} (x : α 0) (q : ∀ i, α i) (p : ∀ i : Fin n, α i.succ) (i : Fin n)
  (y : α i.succ) (z : α 0)

/-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple. -/
def fin_cons (x : α 0) (p : ∀ i : Fin n, α i.succ) : ∀ i, α i := fun j ↦ Fin.cases x p j

def v1 := ![1,2,3]
#eval fin_cons 0 v1  --want this to be ![0,1,2,3]

[Eric Wieser]

#eval (fin_cons 0 v1 : Fin _ → ℕ) works

[Eric Wieser]

But also the function you want here is

Vivek Rajesh Joshi said:

I searched for such a function and found Fin.cons, but I don't understand how to get it to work.

The function you found is identical to the one you wrote:

example : @fin_cons = @Fin.cons := rfl

[Eric Wieser]

Probably you want docs#Matrix.vecCons, which is less general but avoids the need for the ( : Fin _ → ℕ) type ascription

[Vivek Rajesh Joshi]

Oh yea, I wanted to show the function in the mwe but under a different name. Thanks, I'll have a look at the vec_cons function