def cap_unit

bendtorch-core@0.1.0.0 · src/storage/route.bend:8

import Base
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

8def cap_unit(+d: Nat, +h: {Nat.is_le(d, 20n) == True{} : Bool}) -> {U32{Arith.unit(32n, d)} == Size.capacity(d) : U32}:
9  match d:
10    case 0n:
11      {==}
12    case 1n+d1:
13      match d1:
14        case 0n:
15          {==}
16        case 1n+d2:
17          match d2:
18            case 0n:
19              {==}
20            case 1n+d3:
21              match d3:
22                case 0n:
23                  {==}
24                case 1n+d4:
25                  match d4:
26                    case 0n:
27                      {==}
28                    case 1n+d5:
29                      match d5:
30                        case 0n:
31                          {==}
32                        case 1n+d6:
33                          match d6:
34                            case 0n:
35                              {==}
36                            case 1n+d7:
37                              match d7:
38                                case 0n:
39                                  {==}
40                                case 1n+d8:
41                                  match d8:
42                                    case 0n:
43                                      {==}
44                                    case 1n+d9:
45                                      match d9:
46                                        case 0n:
47                                          {==}
48                                        case 1n+d10:
49                                          match d10:
50                                            case 0n:
51                                              {==}
52                                            case 1n+d11:
53                                              match d11:
54                                                case 0n:
55                                                  {==}
56                                                case 1n+d12:
57                                                  match d12:
58                                                    case 0n:
59                                                      {==}
60                                                    case 1n+d13:
61                                                      match d13:
62                                                        case 0n:
63                                                          {==}
64                                                        case 1n+d14:
65                                                          match d14:
66                                                            case 0n:
67                                                              {==}
68                                                            case 1n+d15:
69                                                              match d15:
70                                                                case 0n:
71                                                                  {==}
72                                                                case 1n+d16:
73                                                                  match d16:
74                                                                    case 0n:
75                                                                      {==}
76                                                                    case 1n+d17:
77                                                                      match d17:
78                                                                        case 0n:
79                                                                          {==}
80                                                                        case 1n+d18:
81                                                                          match d18:
82                                                                            case 0n:
83                                                                              {==}
84                                                                            case 1n+d19:
85                                                                              match d19:
86                                                                                case 0n:
87                                                                                  {==}
88                                                                                case 1n+d20:
89                                                                                  match d20:
90                                                                                    case 0n:
91                                                                                      {==}
92                                                                                    case 1n+d21:
93                                                                                      Empty.absurd({U32{Arith.unit(32n, 21n+d21)} == Size.capacity(21n+d21) : U32}, Arith.clash(h))