def app8

lawful-words@0.1.0.0 · proof_zb.bend:21

import lawful-words@0.1.0.0/proof_zb.bend as ProofZb

import Base

21# Eight bits x in front of r.
22def app8(-n: Nat, x: Word(8n), r: Word(n)) -> Word(Nat.add(8n, n)):
23  match x:
24    case WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}:
25      WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, r}}}}}}}}

Uses (5)

Used by (14)