def shift_value

bendtorch-core@0.1.0.0 · src/shape/index_proofs.bend:63

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

63def shift_value(+a: Nat, +b: Nat, +index: Shape.Fin(b)) -> {Shape.Fin.value(Nat.add(a, b), Shape.Fin.shift(a, b, index)) == Nat.add(a, Shape.Fin.value(b, index)) : Nat}:
64  match a:
65    case 0n:
66      {==}
67    case 1n+p:
68      %shift_value(p, b, index) : {1n+Shape.Fin.value(Nat.add(p, b), Shape.Fin.shift(p, b, index)) == 1n+_ : Nat}
69      {==}