def left_value

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

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

51def left_value(+a: Nat, +b: Nat, +index: Shape.Fin(a)) -> {Shape.Fin.value(Nat.add(a, b), Shape.Fin.left(a, b, index)) == Shape.Fin.value(a, index) : Nat}:
52  match a:
53    case 0n:
54      match index:
55    case 1n+p:
56      match index:
57        case Shape.FZero{}:
58          {==}
59        case Shape.FNext{+previous}:
60          %left_value(p, b, previous) : {1n+Shape.Fin.value(Nat.add(p, b), Shape.Fin.left(p, b, previous)) == 1n+_ : Nat}
61          {==}