def Goal

stelliferous@0.0.2.0 · proofs/u32_shift.bend:25

import Base

25def Goal(+w: Word(32n),+c: Bool) -> Type:
26  {U32.is_lt(U32{w},2147483648) == True{} : Bool} -> {Word.shl.out(32n,c,w) == (False{},Word.shl.put(32n,c,w)) : Bool & Word(32n)}