def pick_succ

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:273

import Base

273def pick_succ(+c: Bool, +p: Nat, +q: Nat) -> {Bool.pick(Nat, c, 1n+p, 1n+q) == 1n+Bool.pick(Nat, c, p, q) : Nat}:
274  match c:
275    case True{}:
276      {==}
277    case False{}:
278      {==}