News
Lecture errata : Array index function names
Written on 03.11.2026 22:25 by Shreyas Srinivas
Hi all,
As you might recall, I mentioned that the Array.get functions appear to have changed as I got stuck there for a moment.
Previously there were three functions: Array.get (a[i]) , Array.get! (a[i]!), and Array.getD (a[i]?). These have respectively become Array.getInternal, Array.get!Internal, and Array.getD
Nevertheless they retain the previous type signatures and you can see from the docstring of get!Internal that it accepts only the Nat index i and if the index is out of bounds, it "panics". In lean terms, this means the function returns the `default` value from the `Inhabited` typeclass.
Best Regards,
Shreyas