def naturals_drop

bendtorch-core@0.1.0.0 · src/shape/coordinate_proofs.bend:173

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

173def naturals_drop(+values: List<&2, U32>, +count: Nat) -> {Shape.naturals(List.drop(&2, U32, values, count)) == List.drop(&2, Nat, Shape.naturals(values), count) : List<&2, Nat>}:
174  match values count:
175    case Nil{} count:
176      {==}
177    case head <> tail 0n:
178      {==}
179    case head <> tail 1n+rest:
180      naturals_drop(tail, rest)