def transport

stelliferous@0.0.2.0 · proofs/word_width.bend:4

import Base

4def transport(-source: Nat,-target: Nat,value: Word(source),width: {source == target : Nat}) -> Word(target):
5  %width : Word(_)
6  value