def step_eq

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

import Base

686# p + p == 2^(1+d) when p == 2^d
687def step_eq(d: Nat, p: Nat, i1: {p == pow2(d) : Nat}) -> {Nat.add(p, p) == pow2(1n+d) : Nat}:
688  %i1 : {Nat.add(p, p) == Nat.add(_, _) : Nat}
689  {==}