Showing `Fin a.size` on Advent Day 9

Stream: new members

[Palani Johnson]

Hello! Little late the party but I have been going through Advent of Code and i just solved day 9. My solution can be found here. If you look at both condense! functions you will see I am using Array.get? to get values at an array index. I believe I should be able to use Array.get as my indexes should never be out of bounds but I'm struggling to prove Fin a.size. Any hints on where to start with this?

[Matt Diamond]

I would've defined the left and right arguments as having type Fin fileArray.size. That would solve your problem. Of course you would need to do additional work to prove those constraints whenever you call the function, but that's kind of the point: you show that the original call satisifies the contraints, and then show that the recursive calls continue to satisfy those constraints.

[Matt Diamond]

Also, you should change if left >= right then to if h : left >= right then so you can make use of h : left < right in the else block.

[Matt Diamond]

However, if you don't care about proofs and you just want to be able to get the value without jumping through hoops, there's always Array.get! which will panic if it's out of bounds... the only requirement is to show that the return type is Inhabited

[Palani Johnson]

Thank you for your reply! I originally tried Fin fileArray.size using Array.get but just didn't know how to get the code to compile. Ill try using if h : since seems to do what i want it to