def word_at_front

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:922

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws

922def word_at_front(+values: List<&2, F32>, +word: F32, +position: Nat,
923  below: {Nat.is_lt(position, List.length(&2, F32, values)) == True{} : Bool}) ->
924  {ReduceLaws.word_at(List.append(&2, F32, values, [word]), position) == ReduceLaws.word_at(values, position) : Maybe<&2, F32>}:
925  match values position:
926    case Nil{} _:
927      Empty.absurd({ReduceLaws.word_at([word], position) == None{} : Maybe<&2, F32>}, Arith.lt_zero(position, below))
928    case +value <> +rest 0n:
929      {==}
930    case +value <> +rest 1n+next:
931      word_at_front(rest, word, next, below)