def sign_threshold

bend-collections-laws-crypto@1.0.0.0 · spec/lib/numeric.bend:26

import Base

26def sign_threshold(n: Nat) -> Word(1n+n):
27  match n:
28    case 0n:
29      WCon{True{}, WNil{}}
30    case 1n+p:
31      WCon{False{}, sign_threshold(p)}