def word_at_front

bendtorch-core@0.1.0.0 · src/autograd/reduce_fold_PROOF.bend:78

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

78def word_at_front(+values: List<&2, F32>, +word: F32, +position: Nat,
79  below: {Nat.is_lt(position, List.length(&2, F32, values)) == True{} : Bool}) ->
80  {ReduceLaws.word_at(List.append(&2, F32, values, [word]), position) == ReduceLaws.word_at(values, position) : Maybe<&2, F32>}:
81  match values position:
82    case Nil{} _:
83      Empty.absurd({ReduceLaws.word_at([word], position) == None{} : Maybe<&2, F32>}, Arith.lt_zero(position, below))
84    case +value <> +rest 0n:
85      {==}
86    case +value <> +rest 1n+next:
87      word_at_front(rest, word, next, below)