Word.shl.out: def of Base Import: import Base Lines 1293-1300 of Base/base.bend: https://jend.leeeet.dev/read.txt?path=Base/base.bend&start_line=1293&end_line=1300 import Base def Word.shl.out(n: Nat, c: Bool, w: Word(n)) -> Bool & Word(n): match n: case 0n: (c, WNil{}) case 1n+p: match w: case WCon{b, t}: Word.shl.out.con(p, c, Word.shl.out(p, b, t)) Uses (8): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl.out.con