def sp.blk

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:188

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

188# splitting the bytes of a block gives the block back
189def sp.blk(b: M.CmBlock, rest: List<&2, U32>) -> {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}:
190  match b:
191    case M.CmBlock{U32{WCon{p0, WCon{p1, WCon{p2, WCon{p3, WCon{p4, WCon{p5, WCon{p6, WCon{p7, WCon{p8, WCon{p9, WCon{p10, WCon{p11, WCon{p12, WCon{p13, WCon{p14, WCon{p15, WCon{p16, WCon{p17, WCon{p18, WCon{p19, WCon{p20, WCon{p21, WCon{p22, WCon{p23, WCon{p24, WCon{p25, WCon{p26, WCon{p27, WCon{p28, WCon{p29, WCon{p30, WCon{p31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{q0, WCon{q1, WCon{q2, WCon{q3, WCon{q4, WCon{q5, WCon{q6, WCon{q7, WCon{q8, WCon{q9, WCon{q10, WCon{q11, WCon{q12, WCon{q13, WCon{q14, WCon{q15, WCon{q16, WCon{q17, WCon{q18, WCon{q19, WCon{q20, WCon{q21, WCon{q22, WCon{q23, WCon{q24, WCon{q25, WCon{q26, WCon{q27, WCon{q28, WCon{q29, WCon{q30, WCon{q31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{r0, WCon{r1, WCon{r2, WCon{r3, WCon{r4, WCon{r5, WCon{r6, WCon{r7, WCon{r8, WCon{r9, WCon{r10, WCon{r11, WCon{r12, WCon{r13, WCon{r14, WCon{r15, WCon{r16, WCon{r17, WCon{r18, WCon{r19, WCon{r20, WCon{r21, WCon{r22, WCon{r23, WCon{r24, WCon{r25, WCon{r26, WCon{r27, WCon{r28, WCon{r29, WCon{r30, WCon{r31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s0, WCon{s1, WCon{s2, WCon{s3, WCon{s4, WCon{s5, WCon{s6, WCon{s7, WCon{s8, WCon{s9, WCon{s10, WCon{s11, WCon{s12, WCon{s13, WCon{s14, WCon{s15, WCon{s16, WCon{s17, WCon{s18, WCon{s19, WCon{s20, WCon{s21, WCon{s22, WCon{s23, WCon{s24, WCon{s25, WCon{s26, WCon{s27, WCon{s28, WCon{s29, WCon{s30, WCon{s31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
192      {==}