def pack_value

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

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

71def pack_value(+a: Nat, +b: Nat, +first: Shape.Fin(a), +last: Shape.Fin(b)) -> {Shape.Fin.value(Nat.mul(a, b), Shape.Fin.pack(a, b, (first, last))) == Nat.add(Nat.mul(Shape.Fin.value(a, first), b), Shape.Fin.value(b, last)) : Nat}:
72  match a:
73    case 0n:
74      match first:
75    case 1n+p:
76      match first:
77        case Shape.FZero{}:
78          left_value(b, Nat.mul(p, b), last)
79        case Shape.FNext{+previous}:
80          %add_assoc(b, Nat.mul(Shape.Fin.value(p, previous), b), Shape.Fin.value(b, last)) : {Shape.Fin.value(Nat.add(b, Nat.mul(p, b)), Shape.Fin.shift(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last)))) == _ : Nat}
81          %pack_value(p, b, previous, last) : {Shape.Fin.value(Nat.add(b, Nat.mul(p, b)), Shape.Fin.shift(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last)))) == Nat.add(b, _) : Nat}
82          shift_value(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last)))