law ab0

lawful-fields@0.1.1.0 · proof_digits.bend:547

import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigits

import Base

547law ab0:
548  for +n: U32
549  for +hs: {U32.is_lt(n, 10) == False{} : Bool}
550  for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(0n))) == True{} : Bool}
551  Empty

Uses (11)

Used by (2)