law get_out

minebender-game@1.0.0.0 · proof_base.bend:404

import Base

404# Past its end, a list has nothing.
405law get_out:
406  for -A: Data
407  for +xs: List<&2, A>
408  for +i: Nat
409  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == False{} : Bool}
410  {List.get(&2, A, xs, i) == None{} : Maybe<&2, A>}