def truncate

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:6

import Base

6def truncate(n: Nat,w: Word(1n+n)) -> Word(n):
7  match n:
8    case 0n:
9      WNil{}
10    case 1n+p:
11      WCon{b,t} = w
12      WCon{b,truncate(p,t)}