def app_len

bend-ml-tensor-array@0.1.19.0 · main.bend:1804

import Base

1804# appending adds the lengths
1805def app_len(+xs: List<&2, F32>, +ys: List<&2, F32>) -> {List.length(&2, F32, List.append(&2, F32, xs, ys)) == Nat.add(List.length(&2, F32, xs), List.length(&2, F32, ys)) : Nat}:
1806  match xs:
1807    case Nil{}:
1808      {==}
1809    case Con{h, t}:
1810      %app_len(t, ys) : {1n+List.length(&2, F32, List.append(&2, F32, t, ys)) == 1n+_ : Nat}
1811      {==}