Spraying houses with SIL-y strings on Mischief Night on Nostr: ok... this is kinda blowing my mind right now: in Lean, defining a list of items and ...

ok... this is kinda blowing my mind right now: in Lean, defining a list of items and then attempting to use an invalid index to access an item results in a _compile-time_ error, not a runtime error.

https://lean-lang.org/functional_programming_in_lean/Interlude___-Propositions___-Proofs___-and-Indexing/#props-proofs-indexing