Numeric.Numeric.full: def of gralha-bendquest@0.1.0.0 Import: import gralha-bendquest@0.1.0.0/numeric.bend as Numeric Lines 21-30 of gralha-bendquest@0.1.0.0/numeric.bend: https://jend.leeeet.dev/read.txt?path=gralha-bendquest@0.1.0.0/numeric.bend&start_line=21&end_line=30 import Base def Numeric.full(n: Nat, w: Word(n)) -> Bool: match n: case Zero{}: True{} case Succ{p}: match w: case WCon{False{}, tail}: False{} case WCon{True{}, tail}: Numeric.full(p, tail) Uses (4): 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=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con