Proof on array indices

Stream: new members

[Jesse Wright]

I'm trying to work out how to replace the sorry in the following definition with a proof.

The main hurdle I am hitting is how to state and use the hypothesis h: t.size = 1 within the if condition.

def get(t : Array String) : String := if t.size = 1 then t.get ⟨0, sorry⟩ else ""

[Henrik Böving]

if h:t.size = 1 then ... will get you the hypothesis in scope