def len_step

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

import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray

import Base

1794# s == 1 + (p + (1 + l))  ->  s == 2 + (p + l)
1795def len_step(-s: Nat, +p: Nat, +l: Nat, e: {s == 1n+Nat.add(p, 1n+l) : Nat}) -> {s == 2n+Nat.add(p, l) : Nat}:
1796  %Equal.sym(Nat, 1n+Nat.add(p, l), Nat.add(p, 1n+l), add_succ_r(p, l)) : {s == 1n+_ : Nat}
1797  e

Uses (4)

Used by (3)