def word_presence

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:525

import Base
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws

525def word_presence(+values: List<&2, F32>, +position: Nat) ->
526  {Nat.is_lt(position, List.length(&2, F32, values)) == TransformProof.maybe_present(Laws.word_at(values, position)) : Bool}:
527  match values position:
528    case Nil{} 0n:
529      {==}
530    case Nil{} 1n+next:
531      {==}
532    case value <> rest 0n:
533      {==}
534    case value <> rest 1n+next:
535      word_presence(rest, next)