law get_in

minebender-game@1.0.0.0 · proof_lists.bend:112

import Base

112# Inside a list, an index reads Some of its default.
113law get_in:
114  for -A: Data
115  for +xs: List<&2, A>
116  for +i: Nat
117  for +d: A
118  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
119  {List.get(&2, A, xs, i) == Some{Maybe.default(&2, A, List.get(&2, A, xs, i), d)} : Maybe<&2, A>}