cannot get hypothesis from if then

Stream: new members

[Jem Bishop]

Hi I am trying to define a from_list function for vectors. What I have is

def from_list {α : Type} {n : ℕ} : list α → option (vector α n)
| l     := if l.length = n then some ⟨l, by sorry⟩ else none

within the 'by sorry' i need the hypothesis that l.length=n, which is obviously true due to the if but does not appear in the proof checker.
How would I write this correctly? thanks

[Adam Topaz]

The length of the vector is built into the type itself.

[Rob Lewis]

if h : l.length = n

[Jem Bishop]

@Rob Lewis Thanks! no idea you could do that!

[Adam Topaz]

Oh I see what's happening.

[Adam Topaz]

Is it clear that this function will be useful? How would you actually tell lean about the length of a given list?

[Adam Topaz]

def from_list {α : Type} : Π (l : list α), vector α (l.length) := λ l, ⟨l,rfl⟩

[Jem Bishop]

i just have it as a constant

[Jem Bishop]

my use case is parsing some fixed width string to a vector of characters

[Adam Topaz]

I see.

[Yakov Pechersky]

One can supply the proof of a length of a list for an explicitly given list just by dec_trivial

[Adam Topaz]

Yeah... the code with if then else works because it's decidable :)

Being a mathematician, I still don't think of lean as a programming language