Numeric.sign_threshold: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as Numeric Lines 26-31 of bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend&start_line=26&end_line=31 import Base def sign_threshold(n: Nat) -> Word(1n+n): match n: case 0n: WCon{True{}, WNil{}} case 1n+p: WCon{False{}, sign_threshold(p)} Uses (5): 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 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil